← Mathematical handbook

Rearranged copulas and the Schur order

For a copula E, E↑(u,v)=∫_0^u (∂₁E(·,v))* is the increasing (SI) rearrangement and E↓(u,v)=v-E↑(1-u,v) the decreasing one. We prove that E↑ is a copula, CIS, Schur equivalent to E, and the lower-orthant maximum of {D : D ≤_{∂₁S} E}; E↓ is the minimum. This gives Lemma 2.7 and Proposition 3.1 of Ansari–Rockel.

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

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

Equations

• Verification.condSection C v u = C.conditionalCDF u v

theorem Verification.condSection_nonneg (C : ProbabilityTheory.Copula 2) (v u : ↑unitInterval) : 0 ≤ condSection C v u

theorem Verification.condSection_le_one (C : ProbabilityTheory.Copula 2) (v u : ↑unitInterval) : condSection C v u ≤ 1

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

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

theorem Verification.condSection_one (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : condSection C 1 u = 1

theorem Verification.condSection_zero_ae (C : ProbabilityTheory.Copula 2) : condSection C 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Verification.decRearr_const_zero {s : ℝ} (hs : 0 ≤ s) : decRearr (fun (x : ↑unitInterval) => 0) s = 0

theorem Verification.decRearr_const_one {s : ℝ} (hs : 0 ≤ s) (hs1 : s < 1) : decRearr (fun (x : ↑unitInterval) => 1) s = 1

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

The increasing rearranged copula, as a CDF.

Equations

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

theorem Verification.decRearr_condSection_nonneg (C : ProbabilityTheory.Copula 2) (v s : ↑unitInterval) : 0 ≤ decRearr (condSection C v) ↑s

theorem Verification.decRearr_condSection_le_one (C : ProbabilityTheory.Copula 2) (v s : ↑unitInterval) : decRearr (condSection C v) ↑s ≤ 1

theorem Verification.integrable_decRearr_condSection (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (s : ↑unitInterval) => decRearr (condSection C v) ↑s) MeasureTheory.volume

theorem Verification.upRearrCDF_zero_left (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : upRearrCDF C 0 v = 0

theorem Verification.upRearrCDF_zero_right (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : upRearrCDF C u 0 = 0

theorem Verification.upRearrCDF_one_left (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : upRearrCDF C 1 v = ↑v

theorem Verification.upRearrCDF_one_right (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : upRearrCDF C u 1 = ↑u

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

theorem Verification.upRearrCDF_rectangle (C : ProbabilityTheory.Copula 2) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) : 0 ≤ upRearrCDF C b d - upRearrCDF C a d - upRearrCDF C b c + upRearrCDF C a c

theorem Verification.upRearrCDF_isClassical (C : ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula.IsClassical fun (u : Fin 2 → ↑unitInterval) => upRearrCDF C (u 0) (u 1)

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

The increasing rearranged copula C↑.

Equations

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

theorem Verification.upRearr_cdf (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : (upRearr C).cdf ![u, v] = upRearrCDF C u v

noncomputable def Verification.downRearr (C : ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula 2

The decreasing rearranged copula C↓(u,v)=v-C↑(1-u,v).

Equations

• Verification.downRearr C = (Verification.upRearr C).reflect {0}

theorem Verification.downRearr_cdf (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : (downRearr C).cdf ![u, v] = ↑v - (upRearr C).cdf ![unitInterval.symm u, v]

theorem Verification.upRearr_conditionalCDF (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (upRearr C).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => decRearr (condSection C v) ↑u

The conditional distribution of C↑ is the decreasing rearrangement.

theorem Verification.upRearr_isSI (C : ProbabilityTheory.Copula 2) : (upRearr C).IsSI

Lemma 2.7(ii): C↑ is conditionally increasing (CIS).

theorem Verification.upRearr_schur_equiv (C : ProbabilityTheory.Copula 2) : (upRearr C).SchurLE C ∧ C.SchurLE (upRearr C)

Lemma 2.7(iv): C↑ is Schur equivalent to C.

theorem Verification.downRearr_schur_equiv (C : ProbabilityTheory.Copula 2) : (downRearr C).SchurLE C ∧ C.SchurLE (downRearr C)

theorem Verification.integral_set_le_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (A : Set ↑unitInterval) (hA : MeasurableSet A) (x : ↑unitInterval) (hx : MeasureTheory.volume.real A = ↑x) : ∫ (u : ↑unitInterval) in A, f u ≤ ∫ (s : ↑unitInterval) in Set.Iic x, decRearr f ↑s

Hardy–Littlewood on arbitrary measurable sets.

def Verification.CondRearrSchurLE (D E : ProbabilityTheory.Copula 2) : Prop

The directional Schur order of copulas in its rearrangement form, on conditional CDFs.

Equations

• Verification.CondRearrSchurLE D E = ∀ (v : ↑unitInterval), Verification.RearrSchurLE (Verification.condSection D v) (Verification.condSection E v)

theorem Verification.condRearrSchurLE_iff (D E : ProbabilityTheory.Copula 2) : CondRearrSchurLE D E ↔ D.SchurLE E

theorem Verification.lowerOrthantLE_upRearr_of_schurLE {D E : ProbabilityTheory.Copula 2} (h : D.SchurLE E) : D.LowerOrthantLE (upRearr E)

Lemma 2.7(i): E↑ is the lower-orthant maximum of {D : D ≤_{∂₁S} E}.

theorem Verification.downRearr_lowerOrthantLE_of_schurLE {D E : ProbabilityTheory.Copula 2} (h : D.SchurLE E) : (downRearr E).LowerOrthantLE D

Lemma 2.7(i): E↓ is the lower-orthant minimum of {D : D ≤_{∂₁S} E}.

theorem Verification.upRearr_mem (E : ProbabilityTheory.Copula 2) : (upRearr E).SchurLE E

theorem Verification.downRearr_mem (E : ProbabilityTheory.Copula 2) : (downRearr E).SchurLE E

theorem Verification.schurLE_iff_upRearr (D E : ProbabilityTheory.Copula 2) : D.SchurLE E ↔ (upRearr D).LowerOrthantLE (upRearr E)

Proposition 3.1 (i)⇔(ii).

theorem Verification.upRearr_lowerOrthant_iff_downRearr (D E : ProbabilityTheory.Copula 2) : (upRearr D).LowerOrthantLE (upRearr E) ↔ (downRearr E).LowerOrthantLE (downRearr D)

Proposition 3.1 (ii)⇔(iii).