← Copula mathematical handbook

Integral form of the rearrangement lemma

Integral consequences of the primitive comparison lemma. With F = primDev h v and G = rearrDev h v:

• ∫ |F| ≤ ∫ G and ∫ F² ≤ ∫ G² (the L¹ and L² cases of ∫ φ(|F|) ≤ ∫ φ(G)), obtained from the level-set inequality λ{|F| > y} ≤ λ{G > y} through the layer-cake formula;
• the sup-norm statement |F| ≤ max G is abs_primDev_le_max in Copula.Rearrangement.Primitive;
• both integral inequalities are strict when F takes both signs.

Comparison of integrals through level sets

theorem ProbabilityTheory.Copula.integrableOn_measureReal_gt (a : ↑unitInterval → ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => MeasureTheory.volume.real {u : ↑unitInterval | t < a u}) (Set.Ioc 0 1) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_eq_integral_measureReal_gt {a : ↑unitInterval → ℝ} (ha0 : ∀ (u : ↑unitInterval), 0 ≤ a u) (ha1 : ∀ (u : ↑unitInterval), a u ≤ 1) (ham : Measurable a) : ∫ (u : ↑unitInterval), a u = ∫ (t : ℝ) in Set.Ioc 0 1, MeasureTheory.volume.real {u : ↑unitInterval | t < a u}

theorem ProbabilityTheory.Copula.integral_le_of_measure_gt_le {a b : ↑unitInterval → ℝ} (ha0 : ∀ (u : ↑unitInterval), 0 ≤ a u) (ha1 : ∀ (u : ↑unitInterval), a u ≤ 1) (ham : Measurable a) (hb0 : ∀ (u : ↑unitInterval), 0 ≤ b u) (hb1 : ∀ (u : ↑unitInterval), b u ≤ 1) (hbm : Measurable b) (hle : ∀ (y : ℝ), 0 < y → MeasureTheory.volume.real {u : ↑unitInterval | y < a u} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y < b u}) : ∫ (u : ↑unitInterval), a u ≤ ∫ (u : ↑unitInterval), b u

Comparison of integrals of [0,1]-valued functions through their upper level sets.

theorem ProbabilityTheory.Copula.integral_lt_of_measure_gt_lt {a b : ↑unitInterval → ℝ} (ha0 : ∀ (u : ↑unitInterval), 0 ≤ a u) (ha1 : ∀ (u : ↑unitInterval), a u ≤ 1) (ham : Measurable a) (hb0 : ∀ (u : ↑unitInterval), 0 ≤ b u) (hb1 : ∀ (u : ↑unitInterval), b u ≤ 1) (hbm : Measurable b) (hle : ∀ (y : ℝ), 0 < y → MeasureTheory.volume.real {u : ↑unitInterval | y < a u} ≤ MeasureTheory.volume.real {u : ↑unitInterval | y < b u}) {y₀ : ℝ} (hy₀ : 0 < y₀) (hlt : ∀ y ∈ Set.Ioo 0 y₀, MeasureTheory.volume.real {u : ↑unitInterval | y < a u} < MeasureTheory.volume.real {u : ↑unitInterval | y < b u}) : ∫ (u : ↑unitInterval), a u < ∫ (u : ↑unitInterval), b u

Strict comparison: a strict level-set inequality for all small levels gives a strict inequality of integrals.

Application to F and G

theorem ProbabilityTheory.Copula.integral_abs_primDev_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) : ∫ (u : ↑unitInterval), |primDev h v u| ≤ ∫ (u : ↑unitInterval), rearrDev h v u

Primitive comparison, p = 1: ∫ |F| ≤ ∫ G.

theorem ProbabilityTheory.Copula.setOf_lt_sq_primDev {h : ↑unitInterval → ℝ} {v y : ℝ} (hy : 0 ≤ y) : {u : ↑unitInterval | y < primDev h v u ^ 2} = {u : ↑unitInterval | √y < |primDev h v u|}

theorem ProbabilityTheory.Copula.setOf_lt_sq_rearrDev {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) : {u : ↑unitInterval | y < rearrDev h v u ^ 2} = {u : ↑unitInterval | √y < rearrDev h v u}

theorem ProbabilityTheory.Copula.sq_primDev_le_one {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) : primDev h v u ^ 2 ≤ 1

theorem ProbabilityTheory.Copula.sq_rearrDev_le_one {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) : rearrDev h v u ^ 2 ≤ 1

theorem ProbabilityTheory.Copula.integral_sq_primDev_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) : ∫ (u : ↑unitInterval), primDev h v u ^ 2 ≤ ∫ (u : ↑unitInterval), rearrDev h v u ^ 2

Primitive comparison, p = 2: ∫ F² ≤ ∫ G².

theorem ProbabilityTheory.Copula.measure_pos_of_neg_value {F : ↑unitInterval → ℝ} (hF : Continuous F) (hF0 : F 0 = 0) {y : ℝ} (hy : 0 < y) {t : ↑unitInterval} (ht : F t < -y) : 0 < MeasureTheory.volume.real {u : ↑unitInterval | -y < F u ∧ F u < 0}

A nonempty open subset of the unit interval has positive measure; here for the set {-y < F < 0} when F is continuous, vanishes at 0 and takes a value below -y.

theorem ProbabilityTheory.Copula.integral_abs_primDev_lt {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {t₁ t₂ : ↑unitInterval} (h₁ : 0 < primDev h v t₁) (h₂ : primDev h v t₂ < 0) : ∫ (u : ↑unitInterval), |primDev h v u| < ∫ (u : ↑unitInterval), rearrDev h v u

Primitive comparison, strict p = 1: if F takes both signs, then ∫ |F| < ∫ G.

theorem ProbabilityTheory.Copula.integral_sq_primDev_lt {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) {t₁ t₂ : ↑unitInterval} (h₁ : 0 < primDev h v t₁) (h₂ : primDev h v t₂ < 0) : ∫ (u : ↑unitInterval), primDev h v u ^ 2 < ∫ (u : ↑unitInterval), rearrDev h v u ^ 2

Primitive comparison, strict p = 2: if F takes both signs, then ∫ F² < ∫ G².