Documentation

Copula.Rearrangement.SI

← Copula mathematical handbook

The SI rearrangement of a copula #

For a bivariate copula C, the SI rearrangement of Strothmann, Dette and Siburg (Rearranged dependence measures, Bernoulli, 2024) is C↑(u,v) = ∫_0^u (∂₁C(·,v))↓(t) dt: the conditional distribution functions u ↦ P(V ≤ v | U = u) are rearranged decreasingly in the conditioning variable.

This file constructs upRearr C = C↑ and proves: C↑ is a copula, it is stochastically increasing (hence Π ≤ C↑), C ≤ C↑, its conditional CDFs are the decreasing rearrangements of those of C, it is Schur equivalent to C, and ξ(C↑) = ξ(C). Sectionwise norm inequalities follow from the primitive comparison lemma in Copula.Rearrangement.PrimitiveIntegral; see Copula.Measures.Bounds.

noncomputable def ProbabilityTheory.Copula.condSection (C : Copula 2) (v : ↑unitInterval) :

↑unitInterval → ℝ

The conditional section u ↦ P(V ≤ v | U = u).

Equations

C.condSection v u = C.conditionalCDF u v

Instances For

theorem ProbabilityTheory.Copula.condSection_nonneg (C : Copula 2) (v u : ↑unitInterval) :

0 ≤ C.condSection v u

theorem ProbabilityTheory.Copula.condSection_le_one (C : Copula 2) (v u : ↑unitInterval) :

C.condSection v u ≤ 1

theorem ProbabilityTheory.Copula.condSection_measurable (C : Copula 2) (v : ↑unitInterval) :

Measurable (C.condSection v)

theorem ProbabilityTheory.Copula.condSection_mono (C : Copula 2) {v w : ↑unitInterval} (h : v ≤ w) (u : ↑unitInterval) :

C.condSection v u ≤ C.condSection w u

theorem ProbabilityTheory.Copula.integral_condSection (C : Copula 2) (v : ↑unitInterval) :

∫ (u : ↑unitInterval), C.condSection v u = ↑v

theorem ProbabilityTheory.Copula.cdf_eq_integral_condSection (C : Copula 2) (u v : ↑unitInterval) :

C.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, C.condSection v t

theorem ProbabilityTheory.Copula.condSection_one (C : Copula 2) (u : ↑unitInterval) :

C.condSection 1 u = 1

theorem ProbabilityTheory.Copula.condSection_zero_ae (C : Copula 2) :

C.condSection 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

noncomputable def ProbabilityTheory.Copula.upRearrCDF (C : Copula 2) (u v : ↑unitInterval) :

The SI rearranged copula, as a CDF.

Equations

C.upRearrCDF u v = ∫ (s : ↑unitInterval) in Set.Iic u, ProbabilityTheory.Copula.decRearr (C.condSection v) ↑s

Instances For

theorem ProbabilityTheory.Copula.decRearr_condSection_nonneg (C : Copula 2) (v s : ↑unitInterval) :

0 ≤ decRearr (C.condSection v) ↑s

theorem ProbabilityTheory.Copula.decRearr_condSection_le_one (C : Copula 2) (v s : ↑unitInterval) :

decRearr (C.condSection v) ↑s ≤ 1

theorem ProbabilityTheory.Copula.integrable_decRearr_condSection (C : Copula 2) (v : ↑unitInterval) :

MeasureTheory.Integrable (fun (s : ↑unitInterval) => decRearr (C.condSection v) ↑s) MeasureTheory.volume

theorem ProbabilityTheory.Copula.upRearrCDF_zero_left (C : Copula 2) (v : ↑unitInterval) :

C.upRearrCDF 0 v = 0

theorem ProbabilityTheory.Copula.upRearrCDF_zero_right (C : Copula 2) (u : ↑unitInterval) :

C.upRearrCDF u 0 = 0

theorem ProbabilityTheory.Copula.upRearrCDF_one_left (C : Copula 2) (v : ↑unitInterval) :

C.upRearrCDF 1 v = ↑v

theorem ProbabilityTheory.Copula.upRearrCDF_one_right (C : Copula 2) (u : ↑unitInterval) :

C.upRearrCDF u 1 = ↑u

theorem ProbabilityTheory.Copula.decRearr_condSection_mono (C : Copula 2) {v w : ↑unitInterval} (h : v ≤ w) (s : ↑unitInterval) :

decRearr (C.condSection v) ↑s ≤ decRearr (C.condSection w) ↑s

theorem ProbabilityTheory.Copula.upRearrCDF_rectangle (C : Copula 2) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) :

0 ≤ C.upRearrCDF b d - C.upRearrCDF a d - C.upRearrCDF b c + C.upRearrCDF a c

theorem ProbabilityTheory.Copula.upRearrCDF_isClassical (C : Copula 2) :

IsClassical fun (u : Fin 2 → ↑unitInterval) => C.upRearrCDF (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.upRearr (C : Copula 2) :

The SI rearrangement C↑ of a copula.

Equations

C.upRearr = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => C.upRearrCDF (u 0) (u 1)) ⋯

Instances For

theorem ProbabilityTheory.Copula.upRearr_cdf (C : Copula 2) (u v : ↑unitInterval) :

C.upRearr.cdf ![u, v] = C.upRearrCDF u v

theorem ProbabilityTheory.Copula.upRearr_cdf_eq_integral (C : Copula 2) (u v : ↑unitInterval) :

C.upRearr.cdf ![u, v] = ∫ (s : ↑unitInterval) in Set.Iic u, decRearr (C.condSection v) ↑s

theorem ProbabilityTheory.Copula.upRearr_conditionalCDF (C : Copula 2) (v : ↑unitInterval) :

(fun (u : ↑unitInterval) => C.upRearr.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => decRearr (C.condSection v) ↑u

The conditional distribution functions of C↑ are the decreasing rearrangements of those of C.

theorem ProbabilityTheory.Copula.upRearr_isSI (C : Copula 2) :

C↑ is stochastically increasing.

theorem ProbabilityTheory.Copula.upRearr_isPQD (C : Copula 2) :

C.upRearr.IsPQD

C↑ is positively quadrant dependent, i.e. Π ≤ C↑.

theorem ProbabilityTheory.Copula.cdf_le_upRearr (C : Copula 2) (u v : ↑unitInterval) :

C.cdf ![u, v] ≤ C.upRearr.cdf ![u, v]

C ≤ C↑ pointwise (Hardy–Littlewood).

theorem ProbabilityTheory.Copula.lowerOrthantLE_upRearr (C : Copula 2) :

C.LowerOrthantLE C.upRearr

theorem ProbabilityTheory.Copula.upRearr_schur_equiv (C : Copula 2) :

C.upRearr.SchurLE C ∧ C.SchurLE C.upRearr

C↑ is Schur equivalent to C: every conditional section is equimeasurable with its rearrangement.

theorem ProbabilityTheory.Copula.chatterjeeXi_upRearr (C : Copula 2) :

C.upRearr.chatterjeeXi = C.chatterjeeXi

The SI rearrangement leaves Chatterjee's xi unchanged.