← Mathematical handbook

Chatterjee xi for Ali–Mikhail–Haq copulas

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

theorem Verification.amh_conditionalCDF_of_den_pos {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (v : ↑unitInterval) (hd : ∀ (u : ↑unitInterval), 0 < amhDen θ ↑u ↑v) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.amh θ hmin hmax).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => amhPartial θ ↑u ↑v

theorem Verification.amh_conditionalCDF {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.amh θ hmin ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => amhPartial θ ↑u ↑v

theorem Verification.integral_amhPartial_sq_of_den_pos {θ : ℝ} (v : ↑unitInterval) (hden : ∀ u ∈ Set.Icc 0 1, 0 < amhDen θ u ↑v) : ∫ (u : ↑unitInterval), amhPartial θ ↑u ↑v ^ 2 = ↑v ^ 2 * ((1 - θ * (1 - ↑v)) ^ 2 + (1 - θ * (1 - ↑v)) + 1) / (3 * (1 - θ * (1 - ↑v)))

theorem Verification.integral_amhPartial_sq {θ : ℝ} (hθ : θ < 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), amhPartial θ ↑u ↑v ^ 2 = ↑v ^ 2 * ((1 - θ * (1 - ↑v)) ^ 2 + (1 - θ * (1 - ↑v)) + 1) / (3 * (1 - θ * (1 - ↑v)))

theorem Verification.amh_xi_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi = (6 * ∫ (v : ↑unitInterval), ↑v ^ 2 * ((1 - θ * (1 - ↑v)) ^ 2 + (1 - θ * (1 - ↑v)) + 1) / (3 * (1 - θ * (1 - ↑v)))) - 2

theorem Verification.amh_chatterjeeXi {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi = -θ / 6 - 2 / 3 + 3 / θ - 2 / θ ^ 2 - 2 * (θ - 1) ^ 2 * Real.log (1 - θ) / θ ^ 3

theorem Verification.amh_chatterjeeXi_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).chatterjeeXi = 0

theorem Verification.amh_chatterjeeXi_one : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).chatterjeeXi = 1 / 6

theorem Verification.amh_xi_regular_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi = 2 * θ ^ 2 * ∫ (v : ↑unitInterval), ↑v ^ 2 * (1 - ↑v) ^ 2 / (1 - θ * (1 - ↑v))

theorem Verification.amh_xi_bound_near_zero {θ : ℝ} (hmin : -1 ≤ θ) (hhalf : θ ≤ 1 / 2) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi ≤ 4 * θ ^ 2

theorem Verification.amh_xi_tendsto_zero {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hmin : ∀ (x : A), -1 ≤ θ x) (hmax : ∀ (x : A), θ x ≤ 1) (hθ : Filter.Tendsto θ l (nhds 0)) : Filter.Tendsto (fun (x : A) => (ProbabilityTheory.Copula.amh (θ x) ⋯ ⋯).chatterjeeXi) l (nhds 0)