← Mathematical handbook

Lower semilinear copulas and their xi--footrule bound

The standard lower semilinear representation is C(u,v)=min(u,v) q(max(u,v)), where q(t)/t is nonincreasing for positive t. The chosen value q(0) does not change the copula. This condition is the usual diagonal constraint delta(t)/t^2.

structure Verification.LowerSemilinearData (C : ProbabilityTheory.Copula 2) : Type

• q : ↑unitInterval → ℝ
• nonneg (t : ↑unitInterval) : 0 ≤ self.q t
• ratio_antitone : AntitoneOn (fun (t : ↑unitInterval) => self.q t / ↑t) (Set.Ioi 0)
• cdf_eq (u v : ↑unitInterval) : C.cdf ![u, v] = ↑(min u v) * self.q (max u v)

def Verification.IsLowerSemilinear (C : ProbabilityTheory.Copula 2) : Prop

Equations

• Verification.IsLowerSemilinear C = Nonempty (Verification.LowerSemilinearData C)

theorem Verification.LowerSemilinearData.cdf_of_le {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (u v : ↑unitInterval) (h : u ≤ v) : C.cdf ![u, v] = ↑u * D.q v

theorem Verification.LowerSemilinearData.cdf_of_ge {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (u v : ↑unitInterval) (h : v ≤ u) : C.cdf ![u, v] = ↑v * D.q u

theorem Verification.LowerSemilinearData.ratio_cross {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (u v : ↑unitInterval) (hu : 0 < u) (huv : u ≤ v) : ↑u * D.q v ≤ ↑v * D.q u

theorem Verification.LowerSemilinearData.section_diff_le {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (u w v : ↑unitInterval) (huw : u ≤ w) : C.cdf ![w, v] - C.cdf ![u, v] ≤ (↑w - ↑u) * D.q v

Every section has Lipschitz constant q(v), even when the LSL copula is not SI.

theorem Verification.LowerSemilinearData.section_lipschitz {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (v : ↑unitInterval) : LipschitzWith ⟨D.q v, ⋯⟩ fun (u : ↑unitInterval) => C.cdf ![u, v]

theorem Verification.LowerSemilinearData.conditionalCDF_le {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (v : ↑unitInterval) : ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v ≤ D.q v

theorem Verification.LowerSemilinearData.square_integral_le {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 ≤ C.cdf ![v, v]

theorem Verification.LowerSemilinearData.xi_le_footrule {C : ProbabilityTheory.Copula 2} (D : LowerSemilinearData C) : C.chatterjeeXi ≤ C.spearmanFootrule

The LSL inequality follows from its section bound, without an SI hypothesis.