← Copula mathematical handbook

Level sets of the primitive and of its rearranged primitive

The level-set step of the primitive comparison lemma: with F = primDev h v and G = rearrDev h v,

λ{|F| > y} ≤ λ{G > y} for every y ≥ 0,

and, when F exceeds y somewhere, the quantitative improvement λ{|F| > y} + λ{-y < F < 0} ≤ λ{G > y} which yields the strict inequalities.

Excursions of a continuous function on the unit interval

theorem ProbabilityTheory.Copula.exists_positive_excursions (F : ℝ → ℝ) (hF : Continuous F) (h0 : F 0 = 0) (h1 : F 1 = 0) {y t : ℝ} (ht : t ∈ Set.Icc 0 1) (hty : y < F t) : ∃ (a : ℝ) (b : ℝ) (c : ℝ) (d : ℝ), 0 ≤ a ∧ a ≤ b ∧ b ≤ c ∧ c ≤ d ∧ d ≤ 1 ∧ F a ≤ 0 ∧ y ≤ F b ∧ y ≤ F c ∧ F d ≤ 0 ∧ (∀ u ∈ Set.Ioo a b, 0 < F u ∧ F u ≤ y) ∧ ∀ u ∈ Set.Ioo c d, 0 < F u ∧ F u ≤ y

For a continuous F on [0,1] with F(0) = F(1) = 0 that exceeds y > 0 at some point, there are intervals (a,b) before and (c,d) after the level set {F ≥ y} on which 0 < F ≤ y, with F ≤ 0 at the outer endpoints and F ≥ y at the inner ones.

The level-set comparison

theorem ProbabilityTheory.Copula.level_bound_of_sets {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {y : ℝ} (E₁ E₂ J : Set ↑unitInterval) (hE₁ : MeasurableSet E₁) (hE₂ : MeasurableSet E₂) (hJ : MeasurableSet J) (h12 : Disjoint E₁ E₂) (hJ1 : Disjoint J E₁) (hJ2 : Disjoint J E₂) (hm₁ : y ≤ (∫ (u : ↑unitInterval) in E₁, h u) - MeasureTheory.volume.real E₁ * v) (hm₂ : (∫ (u : ↑unitInterval) in E₂, h u) - MeasureTheory.volume.real E₂ * v ≤ -y) (hb₁ : ∀ u ∈ E₁, |primDev h v u| ≤ y) (hb₂ : ∀ u ∈ E₂, |primDev h v u| ≤ y) (hbJ : ∀ u ∈ J, |primDev h v u| ≤ y) : MeasureTheory.volume.real {u : ↑unitInterval | y < |primDev h v u|} + MeasureTheory.volume.real J ≤ MeasureTheory.volume.real {u : ↑unitInterval | y ≤ rearrDev h v u}

The key estimate behind the level-set comparison: two disjoint sets on which |F| ≤ y, carrying mass ≥ y and ≤ -y of f = h - v, force λ{|F| > y} + λ(J) ≤ λ{G ≥ y} for every further set J inside {|F| ≤ y} disjoint from both.

theorem ProbabilityTheory.Copula.level_bound_ge {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {y : ℝ} (hy : 0 < y) : MeasureTheory.volume.real {u : ↑unitInterval | y < |primDev h v u|} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y ≤ rearrDev h v u} ∧ ((∃ (t : ↑unitInterval), y < primDev h v t) → MeasureTheory.volume.real {u : ↑unitInterval | y < |primDev h v u|} + MeasureTheory.volume.real {u : ↑unitInterval | -y < primDev h v u ∧ primDev h v u < 0} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y ≤ rearrDev h v u})

The level-set inequality with closed level sets of G, for y > 0, together with the improvement by λ{-y < F < 0} when F exceeds y somewhere.

theorem ProbabilityTheory.Copula.measure_gt_add_le_of_forall {a b : ↑unitInterval → ℝ} {y y₁ : ℝ} (hy : y < y₁) (c : ℝ) (hle : ∀ y' ∈ Set.Ioo y y₁, MeasureTheory.volume.real {u : ↑unitInterval | y' < a u} + c ≤ MeasureTheory.volume.real {u : ↑unitInterval | y' ≤ b u}) : MeasureTheory.volume.real {u : ↑unitInterval | y < a u} + c ≤ MeasureTheory.volume.real {u : ↑unitInterval | y < b u}

Passing from closed to open level sets of b by letting y' ↓ y.

theorem ProbabilityTheory.Copula.measure_abs_primDev_gt_le {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {y : ℝ} (hy : 0 ≤ y) : MeasureTheory.volume.real {u : ↑unitInterval | y < |primDev h v u|} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y < rearrDev h v u}

Level-set comparison: λ{|F| > y} ≤ λ{G > y} for every y ≥ 0.

theorem ProbabilityTheory.Copula.measure_abs_primDev_gt_add_le {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {y : ℝ} (hy : 0 ≤ y) {t : ↑unitInterval} (ht : y < primDev h v t) : MeasureTheory.volume.real {u : ↑unitInterval | y < |primDev h v u|} + MeasureTheory.volume.real {u : ↑unitInterval | -y < primDev h v u ∧ primDev h v u < 0} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y < rearrDev h v u}

Quantitative level-set comparison: when F exceeds y ≥ 0 somewhere, the open set {-y < F < 0} is disjoint from the level set {|F| > y} and both together still fit into {G > y}.