← Mathematical handbook

Schur order of conditional distributions

We use the convex-test characterization of majorization of the functions u ↦ P(V ≤ t | U = u), for every threshold t. Their common mean is t. This compares the predictability of the second coordinate given the first. It is a preorder on copulas, not an antisymmetric order.

def ProbabilityTheory.Copula.SchurLE (C D : Copula 2) : Prop

Directional Schur order, in its continuous convex-test formulation.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SchurLE.refl (C : Copula 2) : C.SchurLE C

theorem ProbabilityTheory.Copula.SchurLE.trans {C D E : Copula 2} (h : C.SchurLE D) (k : D.SchurLE E) : C.SchurLE E

theorem ProbabilityTheory.Copula.integrable_comp_conditionalCDF (C : Copula 2) (t : ↑unitInterval) {φ : ℝ → ℝ} (hφ : Continuous φ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => φ (C.conditionalCDF u t)) MeasureTheory.volume

theorem ProbabilityTheory.Copula.schurLE_iff_of_kernel_ae (C D : Copula 2) (κ η : Kernel ↑unitInterval ↑unitInterval) (hκ : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ) (hη : ⇑D.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑η) : C.SchurLE D ↔ ∀ (t : ↑unitInterval) (φ : ℝ → ℝ), Continuous φ → ConvexOn ℝ (Set.Icc 0 1) φ → ∫ (u : ↑unitInterval), φ ((κ u).real (Set.Iic t)) ≤ ∫ (u : ↑unitInterval), φ ((η u).real (Set.Iic t))

Conditional-kernel versions may be replaced almost everywhere.

theorem ProbabilityTheory.Copula.schurLE_of_rearrangement (C D : Copula 2) {r : ↑unitInterval → ↑unitInterval} (hr : MeasureTheory.MeasurePreserving r MeasureTheory.volume MeasureTheory.volume) (h : ∀ (t : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u t) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => D.conditionalCDF (r u) t) : C.SchurLE D ∧ D.SchurLE C

Measure-preserving reparametrization of conditional CDFs preserves Schur equivalence.

theorem ProbabilityTheory.Copula.schurLE_independence (C : Copula 2) : (independence 2).SchurLE C

Independence is a least element, by Jensen's inequality.

theorem ProbabilityTheory.Copula.integral_convex_conditionalCDF_le (C : Copula 2) (t : ↑unitInterval) {φ : ℝ → ℝ} (hc : Continuous φ) (hv : ConvexOn ℝ (Set.Icc 0 1) φ) : ∫ (u : ↑unitInterval), φ (C.conditionalCDF u t) ≤ (1 - ↑t) * φ 0 + ↑t * φ 1

The chord through the endpoint values bounds a convex conditional functional.

theorem ProbabilityTheory.Copula.integral_conditionalCDF_of_function (D : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, x 1 = f (x 0)) (t : ↑unitInterval) (φ : ℝ → ℝ) : ∫ (u : ↑unitInterval), φ (D.conditionalCDF u t) = (1 - ↑t) * φ 0 + ↑t * φ 1

theorem ProbabilityTheory.Copula.schurLE_of_function (C D : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, x 1 = f (x 0)) : C.SchurLE D

Every copula is below every deterministic dependence in directional Schur order.

theorem ProbabilityTheory.Copula.schurLE_comonotonic (C : Copula 2) : C.SchurLE (comonotonic 2)

theorem ProbabilityTheory.Copula.schurLE_countermonotonic (C : Copula 2) : C.SchurLE countermonotonic

theorem ProbabilityTheory.Copula.SchurLE.chatterjeeXi_le {C D : Copula 2} (h : C.SchurLE D) : C.chatterjeeXi ≤ D.chatterjeeXi

Chatterjee's xi respects the directional Schur preorder.