← Mathematical handbook

noncomputable def Verification.bbInv (θ δ u : ℝ) : ℝ

Equations

• Verification.bbInv θ δ u = (u ^ (-θ) - 1) ^ δ

noncomputable def Verification.bbWeight (θ δ u : ℝ) : ℝ

Equations

• Verification.bbWeight θ δ u = θ * δ * u ^ (-θ - 1) * (u ^ (-θ) - 1) ^ (δ - 1)

noncomputable def Verification.bbDensityReal (θ δ u v : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Verification.bbDensity (θ δ : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Verification.bbDensity θ δ x = Verification.bbDensityReal θ δ ↑(x 0) ↑(x 1)

noncomputable def Verification.bbPartial (θ δ u v : ℝ) : ℝ

Equations

• Verification.bbPartial θ δ u v = -Verification.bbPsiDeriv δ⁻¹ θ⁻¹ (Verification.bbInv θ δ u + Verification.bbInv θ δ v) * Verification.bbWeight θ δ u

noncomputable def Verification.bbRealCDF (θ δ u v : ℝ) : ℝ

Equations

• Verification.bbRealCDF θ δ u v = (1 + (Verification.bbInv θ δ u + Verification.bbInv θ δ v) ^ δ⁻¹) ^ (-θ⁻¹)

theorem Verification.bb_inv_base {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : 0 < u ^ (-θ) - 1

theorem Verification.bbInv_pos {θ δ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : 0 < bbInv θ δ u

theorem Verification.bbWeight_pos {θ δ u : ℝ} (hθ : 0 < θ) (hδ : 0 < δ) (hu : u ∈ Set.Ioo 0 1) : 0 < bbWeight θ δ u

theorem Verification.bbInv_deriv {θ δ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (bbInv θ δ) (-bbWeight θ δ u) u

theorem Verification.bbWeight_continuousAt {θ δ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : ContinuousAt (bbWeight θ δ) u

theorem Verification.bbSecond_continuousAt {p q t : ℝ} (ht : 0 < t) : ContinuousAt (bbSecond p q) t

theorem Verification.bbPartial_deriv {θ δ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (bbPartial θ δ u) (bbDensityReal θ δ u v) v

theorem Verification.bbRealCDF_deriv {θ δ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => bbRealCDF θ δ x v) (bbPartial θ δ u v) u

theorem Verification.bbDensity_measurable (θ δ : ℝ) : Measurable (bbDensity θ δ)

theorem Verification.bbDensityReal_nonneg {θ δ : ℝ} (hθ : 0 < θ) (hδ : 1 ≤ δ) (u v : ℝ) : 0 ≤ bbDensityReal θ δ u v

theorem Verification.bbDensityReal_continuousAt {θ δ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : ContinuousAt (Function.uncurry (bbDensityReal θ δ)) (u, v)

theorem Verification.bbPartial_continuousAt {θ δ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : ContinuousAt (fun (x : ℝ) => bbPartial θ δ x v) u

theorem Verification.bb_toMeasure_density {θ δ : ℝ} (hθ : 0 < θ) (hδ : 1 ≤ δ) : (ProbabilityTheory.Copula.bb1 θ hθ δ hδ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (bbDensity θ δ x)

theorem Verification.bbDensity_mtp2 {θ δ : ℝ} (hθ : 0 < θ) (hδ : 1 ≤ δ) : ProbabilityTheory.IsMTP2 (bbDensity θ δ)

theorem Verification.bb_hasMTP2Density {θ δ : ℝ} (hθ : 0 < θ) (hδ : 1 ≤ δ) : (ProbabilityTheory.Copula.bb1 θ hθ δ hδ).HasMTP2Density