← 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 ∫_{[0,x]} f ≤ ∫_{[0,x]} f*.

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

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

Equations

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

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

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

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

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

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

theorem Verification.distFun_rightContinuous {f : ↑unitInterval → ℝ} (_hf : Measurable f) (c : ℝ) : Filter.Tendsto (distFun f) (nhdsWithin c (Set.Ioi c)) (nhds (distFun f c))

Right continuity of the distribution function.

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

The decreasing rearrangement.

Equations

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

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

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

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

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

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

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

The defining property of the rearrangement.

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

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

Equimeasurability on upper level sets.

theorem Verification.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 Verification.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 Verification.decRearr_congr {f g : ↑unitInterval → ℝ} (h : f =ᵐ[MeasureTheory.volume] g) : decRearr f = decRearr g

theorem Verification.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

Layer-cake formulas on initial segments

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

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

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

theorem Verification.integral_Iic_decRearr {f : ↑unitInterval → ℝ} (_hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (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 Verification.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: an initial segment integral is dominated by that of the rearrangement.