← Copula mathematical handbook

Decreasing rearrangements on the unit interval

For a measurable f : I → ℝ with values in [0,1], the decreasing rearrangement is f↓(s) = inf {c ≥ 0 : λ(f > c) ≤ s}. It is antitone, equimeasurable with f, monotone in f, and satisfies the Hardy–Littlewood inequality ∫_A f ≤ ∫_0^{λ(A)} f↓ for measurable A (the bathtub principle; see e.g. Lieb–Loss, Analysis, Section 3.3, or Bennett–Sharpley, Interpolation of Operators, Chapter 2).

This is the general rearrangement infrastructure used for the SI rearrangement of a copula (Copula.Rearrangement.SI) and for the primitive comparison lemma (Copula.Rearrangement.Primitive).

noncomputable def ProbabilityTheory.Copula.distFun (f : ↑unitInterval → ℝ) (c : ℝ) : ℝ

The distribution function c ↦ λ{f > c} on the unit interval.

Equations

• ProbabilityTheory.Copula.distFun f c = MeasureTheory.volume.real {u : ↑unitInterval | c < f u}

theorem ProbabilityTheory.Copula.distFun_nonneg (f : ↑unitInterval → ℝ) (c : ℝ) : 0 ≤ distFun f c

theorem ProbabilityTheory.Copula.distFun_le_one (f : ↑unitInterval → ℝ) (c : ℝ) : distFun f c ≤ 1

theorem ProbabilityTheory.Copula.distFun_antitone (f : ↑unitInterval → ℝ) : Antitone (distFun f)

theorem ProbabilityTheory.Copula.distFun_of_bound {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) {c : ℝ} (hc : 1 ≤ c) : distFun f c = 0

theorem ProbabilityTheory.Copula.distFun_of_neg {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), 0 ≤ f u) {c : ℝ} (hc : c < 0) : distFun f c = 1

theorem ProbabilityTheory.Copula.distFun_rightContinuous (f : ↑unitInterval → ℝ) (c : ℝ) : Filter.Tendsto (distFun f) (nhdsWithin c (Set.Ioi c)) (nhds (distFun f c))

Right continuity of the distribution function.

noncomputable def ProbabilityTheory.Copula.decRearr (f : ↑unitInterval → ℝ) (s : ℝ) : ℝ

The decreasing rearrangement f↓(s) = inf {c ≥ 0 : λ{f > c} ≤ s} of a [0,1]-valued function.

Equations

• ProbabilityTheory.Copula.decRearr f s = sInf {c : ℝ | 0 ≤ c ∧ ProbabilityTheory.Copula.distFun f c ≤ s}

theorem ProbabilityTheory.Copula.decRearr_set_nonempty {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) {s : ℝ} (hs : 0 ≤ s) : {c : ℝ | 0 ≤ c ∧ distFun f c ≤ s}.Nonempty

theorem ProbabilityTheory.Copula.decRearr_set_bdd (f : ↑unitInterval → ℝ) (s : ℝ) : BddBelow {c : ℝ | 0 ≤ c ∧ distFun f c ≤ s}

theorem ProbabilityTheory.Copula.decRearr_nonneg {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ decRearr f s

theorem ProbabilityTheory.Copula.decRearr_le_one {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) {s : ℝ} (hs : 0 ≤ s) : decRearr f s ≤ 1

theorem ProbabilityTheory.Copula.decRearr_antitoneOn {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) : AntitoneOn (decRearr f) (Set.Ici 0)

theorem ProbabilityTheory.Copula.lt_decRearr_iff {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) {c s : ℝ} (hc : 0 ≤ c) (hs : 0 ≤ s) : c < decRearr f s ↔ s < distFun f c

The defining property of the rearrangement.

theorem ProbabilityTheory.Copula.decRearr_measurable {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) : Measurable fun (s : ↑unitInterval) => decRearr f ↑s

theorem ProbabilityTheory.Copula.volume_lt_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (c : ℝ) : MeasureTheory.volume {s : ↑unitInterval | c < decRearr f ↑s} = MeasureTheory.volume {u : ↑unitInterval | c < f u}

Equimeasurability on upper level sets.

theorem ProbabilityTheory.Copula.map_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) : MeasureTheory.Measure.map (fun (s : ↑unitInterval) => decRearr f ↑s) MeasureTheory.volume = MeasureTheory.Measure.map f MeasureTheory.volume

The pushforward distributions of f and of its rearrangement coincide.

theorem ProbabilityTheory.Copula.integral_comp_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) {φ : ℝ → ℝ} (hφ : Measurable φ) : ∫ (s : ↑unitInterval), φ (decRearr f ↑s) = ∫ (u : ↑unitInterval), φ (f u)

theorem ProbabilityTheory.Copula.decRearr_congr {f g : ↑unitInterval → ℝ} (h : f =ᵐ[MeasureTheory.volume] g) : decRearr f = decRearr g

theorem ProbabilityTheory.Copula.decRearr_mono {f g : ↑unitInterval → ℝ} (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (h : ∀ᵐ (u : ↑unitInterval), f u ≤ g u) {s : ℝ} (hs : 0 ≤ s) : decRearr f s ≤ decRearr g s

theorem ProbabilityTheory.Copula.integrable_comp_of_unit {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) {φ : ℝ → ℝ} (hφ : Continuous φ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => φ (f u)) MeasureTheory.volume

A continuous function of a [0,1]-valued measurable function is integrable.

theorem ProbabilityTheory.Copula.integrable_decRearr {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) : MeasureTheory.Integrable (fun (s : ↑unitInterval) => decRearr f ↑s) MeasureTheory.volume

Layer-cake formulas on initial segments

theorem ProbabilityTheory.Copula.integral_Iic_eq_layercake {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (A : Set ↑unitInterval) : ∫ (u : ↑unitInterval) in A, f u = ∫ (t : ℝ) in Set.Ioc 0 1, MeasureTheory.volume.real (A ∩ {u : ↑unitInterval | t < f u})

theorem ProbabilityTheory.Copula.antitone_measureReal_inter (A : Set ↑unitInterval) (f : ↑unitInterval → ℝ) : Antitone fun (t : ℝ) => MeasureTheory.volume.real (A ∩ {u : ↑unitInterval | t < f u})

theorem ProbabilityTheory.Copula.volume_Iic_inter_lt_decRearr {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (x : ↑unitInterval) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.volume.real (Set.Iic x ∩ {s : ↑unitInterval | t < decRearr f ↑s}) = min (↑x) (distFun f t)

theorem ProbabilityTheory.Copula.integral_Iic_decRearr {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (x : ↑unitInterval) : ∫ (s : ↑unitInterval) in Set.Iic x, decRearr f ↑s = ∫ (t : ℝ) in Set.Ioc 0 1, min (↑x) (distFun f t)

Layer-cake form of the partial integrals of the rearrangement.

theorem ProbabilityTheory.Copula.integral_set_le_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (A : Set ↑unitInterval) (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 (bathtub principle) on arbitrary measurable sets: the integral of f over a set of measure x is dominated by the integral of f↓ over [0, x].

theorem ProbabilityTheory.Copula.integral_Iic_le_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (x : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic x, f u ≤ ∫ (s : ↑unitInterval) in Set.Iic x, decRearr f ↑s

Hardy–Littlewood on initial segments.

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

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