← Mathematical handbook

Families that are unordered in the Schur order

A parameter family starting at the lower Fréchet bound W and tending to M cannot be Schur-monotone in either direction as soon as one member has median conditional energy strictly below 1/2: W and M both have energy 1/2, and the median strip inequality forces energy close to 1/2 near M.

theorem Verification.countermonotonic_median_energy : ∫ (u : ↑unitInterval), ProbabilityTheory.Copula.countermonotonic.conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 = 1 / 2

theorem Verification.not_countermonotonic_schurLE (C : ProbabilityTheory.Copula 2) (hC : ∫ (u : ↑unitInterval), C.conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2) : ¬ProbabilityTheory.Copula.countermonotonic.SchurLE C

A copula with median energy below 1/2 is not Schur-above W.

theorem Verification.not_schurLE_of_tendsto_comonotonic {α : Type u_1} {l : Filter α} [l.NeBot] (C : α → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2) (hC : Filter.Tendsto (fun (a : α) => (C a).cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf]) l (nhds (1 / 2))) (hD : ∫ (u : ↑unitInterval), D.conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2) : ¬∀ (a : α), (C a).SchurLE D

Copulas converging to M at the median eventually are not Schur-below a copula with median energy below 1/2.

theorem Verification.comonotonic_median_cdf : (ProbabilityTheory.Copula.comonotonic 2).cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf] = 1 / 2

Nelsen 2

theorem Verification.nelsen2_two_section (v : ↑unitInterval) (hv : ↑v = 1 / 2) {u : ℝ} (hu : u ∈ Set.Ioo (1 / 4) 1) : (ProbabilityTheory.Copula.nelsen2 2 ⋯).cdfSection v u = 1 - √((1 - u) ^ 2 + (1 - ↑v) ^ 2)

theorem Verification.nelsen2_two_median_energy_lt : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.nelsen2 2 ⋯).conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2

theorem Verification.nelsen2_not_schur_monotone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.nelsen2 θ hθ).SchurLE (ProbabilityTheory.Copula.nelsen2 η ⋯)

theorem Verification.nelsen2_not_schur_antitone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.nelsen2 η ⋯).SchurLE (ProbabilityTheory.Copula.nelsen2 θ hθ)

Genest–Ghoudi (Nelsen 15)

theorem Verification.genestGhoudi_two_section (v : ↑unitInterval) (hv : ↑v = 1 / 2) {u : ℝ} (hu : u ∈ Set.Ioo (1 / 4) 1) : (ProbabilityTheory.Copula.genestGhoudi 2 ⋯).cdfSection v u = (1 - √((1 - √u) ^ 2 + (1 - √↑v) ^ 2)) ^ 2

theorem Verification.genestGhoudi_two_median_energy_lt : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.genestGhoudi 2 ⋯).conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2

theorem Verification.genestGhoudi_not_schur_monotone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.genestGhoudi θ hθ).SchurLE (ProbabilityTheory.Copula.genestGhoudi η ⋯)

theorem Verification.genestGhoudi_not_schur_antitone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.genestGhoudi η ⋯).SchurLE (ProbabilityTheory.Copula.genestGhoudi θ hθ)