Documentation

Papers.AnsariRockel2024.Rearrangement

← Mathematical handbook

Rearrangement-based Schur order (Lemma 2.4, Lemma 2.7, Proposition 3.1) #

The paper defines D ≤_{∂₁S} E by comparing decreasing rearrangements of the partial derivatives ∂₁D(·,v) and ∂₁E(·,v) (Definition 2.3). The library order SchurLE compares the conditional distributions through continuous convex tests. Lemma 2.4 is their equivalence; it combines the almost-everywhere derivative bridge with the Hardy–Littlewood–Pólya theorem on the unit interval.

def Papers.AnsariRockel2024.PaperSchurLE (D E : ProbabilityTheory.Copula 2) :

Definition 2.3: D ≤_{∂₁S} E via decreasing rearrangements of ∂₁D(·,v).

Equations

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

Instances For

def Papers.AnsariRockel2024.PaperSchurBothLE (D E : ProbabilityTheory.Copula 2) :

Definition 2.3: the two-direction order ≤_{∂S}.

Equations

Papers.AnsariRockel2024.PaperSchurBothLE D E = (Papers.AnsariRockel2024.PaperSchurLE D E ∧ Papers.AnsariRockel2024.PaperSchurLE D.transpose E.transpose)

Instances For

theorem Papers.AnsariRockel2024.rearrSchurLE_congr {f f' g g' : ↑unitInterval → ℝ} (hf : f =ᵐ[MeasureTheory.volume] f') (hg : g =ᵐ[MeasureTheory.volume] g') :

Verification.RearrSchurLE f g ↔ Verification.RearrSchurLE f' g'

theorem Papers.AnsariRockel2024.schur_endpoint_trivial (D E : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : v = 0 ∨ v = 1) (φ : ℝ → ℝ) :

∫ (u : ↑unitInterval), φ (D.conditionalCDF u v) = ∫ (u : ↑unitInterval), φ (E.conditionalCDF u v)

theorem Papers.AnsariRockel2024.paperSchurLE_iff (D E : ProbabilityTheory.Copula 2) :

PaperSchurLE D E ↔ D.SchurLE E

Lemma 2.4: the rearrangement Schur order of partial derivatives coincides with the Schur order of conditional distributions (convex-test form).

theorem Papers.AnsariRockel2024.paperSchurBothLE_iff (D E : ProbabilityTheory.Copula 2) :

PaperSchurBothLE D E ↔ D.SchurBothLE E

theorem Papers.AnsariRockel2024.rearranged_extremal (D E : ProbabilityTheory.Copula 2) (h : D.SchurLE E) :

(Verification.downRearr E).LowerOrthantLE D ∧ D.LowerOrthantLE (Verification.upRearr E)

Lemma 2.7(i): E↓ ≤_lo D ≤_lo E↑ for every D ≤_{∂₁S} E, and both bounds belong to the class.

theorem Papers.AnsariRockel2024.rearranged_mem (E : ProbabilityTheory.Copula 2) :

(Verification.upRearr E).SchurLE E ∧ (Verification.downRearr E).SchurLE E

theorem Papers.AnsariRockel2024.rearranged_unique_max (E M : ProbabilityTheory.Copula 2) (hM : M.SchurLE E) (hmax : ∀ (D : ProbabilityTheory.Copula 2), D.SchurLE E → D.LowerOrthantLE M) :

M = Verification.upRearr E

Uniqueness of the lower-orthant maximum and minimum.

theorem Papers.AnsariRockel2024.rearranged_unique_min (E M : ProbabilityTheory.Copula 2) (hM : M.SchurLE E) (hmin : ∀ (D : ProbabilityTheory.Copula 2), D.SchurLE E → M.LowerOrthantLE D) :

M = Verification.downRearr E

theorem Papers.AnsariRockel2024.upRearr_cis (E : ProbabilityTheory.Copula 2) :

(Verification.upRearr E).IsSI

Lemma 2.7(ii): E↑ is CIS.

theorem Papers.AnsariRockel2024.downRearr_formula (E : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) :

(Verification.downRearr E).cdf ![u, v] = ↑v - (Verification.upRearr E).cdf ![unitInterval.symm u, v]

Lemma 2.7(iii): E↓(u,v)=v-E↑(1-u,v).

theorem Papers.AnsariRockel2024.rearranged_schur_equiv (E : ProbabilityTheory.Copula 2) :

((Verification.upRearr E).SchurLE E ∧ E.SchurLE (Verification.upRearr E)) ∧ (Verification.downRearr E).SchurLE E ∧ E.SchurLE (Verification.downRearr E)

Lemma 2.7(iv): E↑ =_{∂₁S} E =_{∂₁S} E↓.

theorem Papers.AnsariRockel2024.upRearr_formula (E : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) :

(Verification.upRearr E).cdf ![u, v] = ∫ (s : ↑unitInterval) in Set.Iic u, Verification.decRearr (fun (t : ↑unitInterval) => deriv (E.cdfSection v) ↑t) ↑s

The increasing rearrangement in explicit form E↑(u,v)=∫_0^u (∂₁E(·,v))*.

theorem Papers.AnsariRockel2024.prop31 (D E : ProbabilityTheory.Copula 2) :

(PaperSchurLE D E ↔ (Verification.upRearr D).LowerOrthantLE (Verification.upRearr E)) ∧ ((Verification.upRearr D).LowerOrthantLE (Verification.upRearr E) ↔ (Verification.downRearr E).LowerOrthantLE (Verification.downRearr D))

Proposition 3.1: D ≤_{∂₁S} E ⇔ D↑ ≤_lo E↑ ⇔ D↓ ≥_lo E↓.