← Copula mathematical handbook

Diagonal fixed points as copula cuts

If C(a,a)=a, each section through the cut agrees with the upper Fréchet bound. The two off-diagonal rectangles are consequently determined. The threshold indicators agree almost surely exactly at such a cut.

theorem ProbabilityTheory.Copula.cdf_right_cut_of_le (C : Copula 2) (a u : ↑unitInterval) (ha : C.diagonal a = ↑a) (hu : u ≤ a) : C.cdf ![u, a] = ↑u

theorem ProbabilityTheory.Copula.cdf_left_cut_of_le (C : Copula 2) (a v : ↑unitInterval) (ha : C.diagonal a = ↑a) (hv : v ≤ a) : C.cdf ![a, v] = ↑v

theorem ProbabilityTheory.Copula.cdf_right_cut_of_ge (C : Copula 2) (a u : ↑unitInterval) (ha : C.diagonal a = ↑a) (hu : a ≤ u) : C.cdf ![u, a] = ↑a

theorem ProbabilityTheory.Copula.cdf_left_cut_of_ge (C : Copula 2) (a v : ↑unitInterval) (ha : C.diagonal a = ↑a) (hv : a ≤ v) : C.cdf ![a, v] = ↑a

theorem ProbabilityTheory.Copula.cdf_right_cut (C : Copula 2) (a u : ↑unitInterval) (ha : C.diagonal a = ↑a) : C.cdf ![u, a] = min ↑u ↑a

theorem ProbabilityTheory.Copula.cdf_left_cut (C : Copula 2) (a v : ↑unitInterval) (ha : C.diagonal a = ↑a) : C.cdf ![a, v] = min ↑a ↑v

theorem ProbabilityTheory.Copula.cdf_cross_cut_lower_upper (C : Copula 2) (a u v : ↑unitInterval) (ha : C.diagonal a = ↑a) (hu : u ≤ a) (hv : a ≤ v) : C.cdf ![u, v] = ↑u

theorem ProbabilityTheory.Copula.cdf_cross_cut_upper_lower (C : Copula 2) (a u v : ↑unitInterval) (ha : C.diagonal a = ↑a) (hu : a ≤ u) (hv : v ≤ a) : C.cdf ![u, v] = ↑v

theorem ProbabilityTheory.Copula.measureReal_threshold_disagreement (C : Copula 2) (a : ↑unitInterval) : C.toMeasure.real {x : Fin 2 → ↑unitInterval | ¬(x 0 ≤ a ↔ x 1 ≤ a)} = 2 * (↑a - C.diagonal a)

Disagreement of the two threshold indicators measures the diagonal's deficit.

theorem ProbabilityTheory.Copula.diagonal_eq_iff_ae_same_side (C : Copula 2) (a : ↑unitInterval) : C.diagonal a = ↑a ↔ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 0 ≤ a ↔ x 1 ≤ a

theorem ProbabilityTheory.Copula.diagonal_eq_iff_measureReal_max_eq_min (C : Copula 2) (a : ↑unitInterval) : C.diagonal a = ↑a ↔ C.toMeasure.real {x : Fin 2 → ↑unitInterval | max (x 0) (x 1) ≤ a} = C.toMeasure.real {x : Fin 2 → ↑unitInterval | min (x 0) (x 1) ≤ a}

theorem ProbabilityTheory.Copula.isClosed_diagonal_fixedPoints (C : Copula 2) : IsClosed {a : ↑unitInterval | C.diagonal a = ↑a}

theorem ProbabilityTheory.Copula.IsNQD.diagonal_lt {C : Copula 2} (h : C.IsNQD) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.diagonal a < ↑a