Documentation

Verification.AMHDensity

← Mathematical handbook

noncomputable def Verification.amhDen (θ u v : ℝ) :

Equations

Verification.amhDen θ u v = 1 - θ * (1 - u) * (1 - v)

Instances For

noncomputable def Verification.amhNum (θ u v : ℝ) :

Equations

Verification.amhNum θ u v = (1 - θ) * Verification.amhDen θ u v + 2 * θ * u * v

Instances For

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

Equations

Verification.amhDensity θ x = Verification.amhNum θ ↑(x 0) ↑(x 1) / Verification.amhDen θ ↑(x 0) ↑(x 1) ^ 3

Instances For

theorem Verification.amhDen_pos {θ u v : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) :

0 < amhDen θ u v

theorem Verification.amhNum_nonneg {θ u v : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) :

0 ≤ amhNum θ u v

theorem Verification.amhDensity_nonneg {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) (x : Fin 2 → ↑unitInterval) :

0 ≤ amhDensity θ x

theorem Verification.continuous_amhDensity {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) :

Continuous (amhDensity θ)

theorem Verification.amhNum_tp2 {θ : ℝ} (hθ : 0 ≤ θ) :

ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => amhNum θ ↑u ↑v

theorem Verification.amhDen_inv_tp2 {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) :

ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => 1 / amhDen θ ↑u ↑v

theorem Verification.isMTP2_amhDensity {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) :

ProbabilityTheory.IsMTP2 (amhDensity θ)

noncomputable def Verification.amhPartial (θ u v : ℝ) :

Equations

Verification.amhPartial θ u v = v * (1 - θ * (1 - v)) / Verification.amhDen θ u v ^ 2

Instances For

theorem Verification.amh_cdf_derivative {θ u v : ℝ} (hd : amhDen θ u v ≠ 0) :

HasDerivAt (fun (x : ℝ) => x * v / amhDen θ x v) (amhPartial θ u v) u

theorem Verification.amh_partial_derivative {θ u v : ℝ} (hd : amhDen θ u v ≠ 0) :

HasDerivAt (fun (y : ℝ) => amhPartial θ u y) (amhNum θ u v / amhDen θ u v ^ 3) v

theorem Verification.integral_amhDensity_second {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) (u v : ↑unitInterval) :

∫ (y : ↑unitInterval) in Set.Iic v, amhDensity θ ![u, y] = amhPartial θ ↑u ↑v

theorem Verification.integral_amhPartial_first {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) (u v : ↑unitInterval) :

∫ (x : ↑unitInterval) in Set.Iic u, amhPartial θ ↑x ↑v = ↑u * ↑v / amhDen θ ↑u ↑v

theorem Verification.amh_toMeasure_density {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) :

(ProbabilityTheory.Copula.amh θ ⋯ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (amhDensity θ x)

theorem Verification.amh_hasMTP2Density {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1) :

(ProbabilityTheory.Copula.amh θ ⋯ ⋯).HasMTP2Density