Decreasing rearrangements f^#

noncomputable def MeasureTheory.rearrangement {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] (f : α → ε) (t : ENNReal) (μ : Measure α) : ENNReal

The decreasing rearrangement function f^#. It equals μ univ for t = 0. Note that unlike the notes, we also define this for t = ∞.

Equations

• MeasureTheory.rearrangement f t μ = sInf {σ : ENNReal | MeasureTheory.distribution f σ μ ≤ t}

@[simp]

theorem MeasureTheory.rearrangement_top {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} : rearrangement f ⊤ μ = 0

theorem MeasureTheory.rearrangement_eq_zero_of_ae_zero_enorm {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {x : ENNReal} (h : enorm ∘ f =ᵐ[μ] 0) : rearrangement f x μ = 0

theorem MeasureTheory.rearrangement_eq_zero_of_ae_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : f =ᵐ[μ] 0) : rearrangement f x μ = 0

@[simp]

theorem MeasureTheory.rearrangement_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] : rearrangement 0 x μ = 0

theorem MeasureTheory.rearrangement_antitone' {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {x y : ENNReal} (h : x ≤ y) : rearrangement f y μ ≤ rearrangement f x μ

theorem MeasureTheory.rearrangement_antitone {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} : Antitone fun (t : ENNReal) => rearrangement f t μ

theorem MeasureTheory.rearrangement_mono_fun {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m : MeasurableSpace α} [ENorm ε] [ENorm ε'] {f : α → ε} {g : α → ε'} {μ : Measure α} {x : ENNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : rearrangement f x μ ≤ rearrangement g x μ

theorem MeasureTheory.rearrangement_le_rearrangement {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m : MeasurableSpace α} [ENorm ε] [ENorm ε'] {f : α → ε} {g : α → ε'} {μ : Measure α} {x y : ENNReal} (h1 : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) (h2 : x ≤ y) : rearrangement f y μ ≤ rearrangement g x μ

theorem MeasureTheory.rearrangment_eq_rearrangement_of_distribution_eq_distribution {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m : MeasurableSpace α} [ENorm ε] [ENorm ε'] {f : α → ε} {μ : Measure α} {β : Type u_4} {m' : MeasurableSpace β} {ν : Measure β} {g : β → ε'} {t : ENNReal} (h : ∀ ⦃s : ENNReal⦄, distribution f s μ = distribution g s ν) : rearrangement f t μ = rearrangement g t ν

theorem MeasureTheory.rearrangement_measurable₀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} : Measurable fun (t : ENNReal) => rearrangement f t μ

theorem MeasureTheory.rearrangement_measurable {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {α' : Type u_4} {m✝ : MeasurableSpace α'} {g : α' → ENNReal} (hg : Measurable g) : Measurable fun (y : α') => rearrangement f (g y) μ

theorem MeasureTheory.rearrangement_distribution_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {x : ENNReal} : rearrangement f (distribution f x μ) μ ≤ x

theorem MeasureTheory.distribution_rearrangement_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {x : ENNReal} : distribution f (rearrangement f x μ) μ ≤ x

theorem MeasureTheory.lt_rearrangement_iff_lt_distribution {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {t y : ENNReal} : y < rearrangement f t μ ↔ t < distribution f y μ

theorem MeasureTheory.rearrangement_le_iff_distribution_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {t y : ENNReal} : rearrangement f t μ ≤ y ↔ distribution f y μ ≤ t

@[simp]

theorem MeasureTheory.distribution_rearrangement_eq_distribution {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {t : ENNReal} : distribution (fun (x : ENNReal) => rearrangement f x μ) t volume = distribution f t μ

@[simp]

theorem MeasureTheory.support_rearrangement_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} : (Function.support fun (x : ENNReal) => rearrangement f x μ) = Set.Iio (μ (Function.support f))

theorem MeasureTheory.ae_eq_zero_of_rearrangement_ae_eq_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (h : (fun (t : ENNReal) => rearrangement f t μ) =ᵐ[volume] 0) : f =ᵐ[μ] 0

theorem MeasureTheory.continuousWithinAt_rearrangement {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {x : ENNReal} : ContinuousWithinAt (fun (x : ENNReal) => rearrangement f x μ) (Set.Ici x) x

theorem MeasureTheory.rearrangement_eq_rearrangement_prod {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_5} [ENorm ε] {f : α → ε} {t : ENNReal} {β : Type u_4} {m' : MeasurableSpace β} {ν : Measure β} [IsProbabilityMeasure ν] : rearrangement f t μ = rearrangement (fun (x : α × β) => f x.1) t (μ.prod ν)

theorem MeasureTheory.rearrangement_indicator_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {X : Set α} : rearrangement (X.indicator f) x μ ≤ (Set.Iio (μ X)).indicator (fun (x : ENNReal) => rearrangement f x μ) x

@[simp]

theorem MeasureTheory.rearrangement_indicator_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {a : ε} : rearrangement (s.indicator (Function.const α a)) x μ = (Set.Iio (μ s)).indicator (Function.const ENNReal ‖a‖ₑ) x

theorem MeasureTheory.rearrangement_const_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {f : α → ENNReal} {a : ENNReal} : rearrangement (a • f) x μ = a * rearrangement f x μ

theorem MeasureTheory.rearrangement_indicator_superlevelSet {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} {t : ENNReal} : rearrangement ((superlevelSet f t).indicator f) x μ = (superlevelSet (fun (x : ENNReal) => rearrangement f x μ) t).indicator (fun (x : ENNReal) => rearrangement f x μ) x

theorem MeasureTheory.rearrangement_indicator_superlevelSet_compl {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {t : ENNReal} (ht : distribution f t μ ≠ ⊤) : rearrangement ((superlevelSet f t)ᶜ.indicator f) x μ = rearrangement f (x + distribution f t μ) μ

theorem MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) (hf' : μ (Function.support f) < ⊤) {s : Set ENNReal} (hs : MeasurableSet s) : μ {x : α | ‖f x‖ₑ ∈ s \ {0}} = volume {x : ENNReal | rearrangement f x μ ∈ s \ {0}}

theorem MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) (hf' : μ (Function.support f) < ⊤) {s : Set ENNReal} (hs : MeasurableSet s) (zero_notin_s : 0 ∉ s) : μ {x : α | ‖f x‖ₑ ∈ s} = volume {x : ENNReal | rearrangement f x μ ∈ s}

theorem MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {s : Set ENNReal} (hs : MeasurableSet s) (zero_notin_s : 0 ∉ s) (h : ∃ (T : ENNReal), (∀ t ∈ s, T < t) ∧ distribution f T μ < ⊤) : μ {x : α | ‖f x‖ₑ ∈ s} = volume {x : ENNReal | rearrangement f x μ ∈ s}

theorem MeasureTheory.measure_enorm_eq_eq_volume_rearrangement_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {a : ENNReal} (ha : distribution f a μ ≠ ⊤) (h : μ {x : α | ‖f x‖ₑ = a} = ⊤) : volume {x : ENNReal | rearrangement f x μ = a} = ⊤

theorem MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {s : Set ENNReal} (hs : MeasurableSet s) (zero_notin_s : 0 ∉ s) (inf_not_mem : sInf s ∉ s) (hs' : ∀ t ∈ s, distribution f t μ < ⊤) : μ {x : α | ‖f x‖ₑ ∈ s} = volume {x : ENNReal | rearrangement f x μ ∈ s}

theorem MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {g : ENNReal → ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) {t : ENNReal} (h : ∃ (T : ENNReal), (∀ s ≤ T, g s ≤ t) ∧ distribution f T μ < ⊤) : distribution (fun (x : α) => g ‖f x‖ₑ) t μ = distribution (g ∘ fun (x : ENNReal) => rearrangement f x μ) t volume

theorem MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) (hf' : ∀ σ > 0, distribution f σ μ < ⊤) {g : ENNReal → ENNReal} {t : ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) : distribution (fun (x : α) => g ‖f x‖ₑ) t μ = distribution (g ∘ fun (x : ENNReal) => rearrangement f x μ) t volume

theorem MeasureTheory.lintegral_comp_rearrangement' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {g : ENNReal → ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) (hg' : ∀ t > 0, distribution f t μ = ⊤ → ∃ S > 0, ∀ y > t, S < g y) : ∫⁻ (x : α), g ‖f x‖ₑ ∂μ = ∫⁻ (t : ENNReal), g (rearrangement f t μ)

theorem MeasureTheory.lintegral_comp_rearrangement_of_distribution_finite {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) (hf' : ∀ t > 0, distribution f t μ ≠ ⊤) {g : ENNReal → ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) : ∫⁻ (x : α), g ‖f x‖ₑ ∂μ = ∫⁻ (t : ENNReal), g (rearrangement f t μ)

theorem MeasureTheory.lintegral_comp_rearrangement {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {g : ENNReal → ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) (hg' : ∀ t > 0, ∃ S > 0, ∀ y > t, S < g y) : ∫⁻ (x : α), g ‖f x‖ₑ ∂μ = ∫⁻ (t : ENNReal), g (rearrangement f t μ)

theorem MeasureTheory.lintegral_comp_rearrangement_of_strictmono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {g : ENNReal → ENNReal} (hg : Measurable g) (g_zero : g 0 = 0) (hg' : StrictMono g) : ∫⁻ (x : α), g ‖f x‖ₑ ∂μ = ∫⁻ (t : ENNReal), g (rearrangement f t μ)

theorem MeasureTheory.lintegral_rearrangement_pow {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) : ∫⁻ (t : ENNReal), rearrangement f t μ ^ p = ∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ

theorem MeasureTheory.lintegral_rearrangement {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : ∫⁻ (t : ENNReal), rearrangement f t μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

theorem MeasureTheory.rearrangement_add_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x y : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f g : α → ε} : rearrangement (f + g) (x + y) μ ≤ rearrangement f x μ + rearrangement g y μ

theorem MeasureTheory.sSup_rearrangement {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} : ⨆ (t : ENNReal), ⨆ (_ : t > 0), rearrangement f t μ = rearrangement f 0 μ

theorem MeasureTheory.rearrangement_zero_eq_eLpNormEssSup {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} : rearrangement f 0 μ = eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm'_rearrangement {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) : eLpNorm' (fun (x : ENNReal) => rearrangement f x μ) p volume = eLpNorm' f p μ

theorem MeasureTheory.setLIntegral_enorm_le_lintegral_rearrangement {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : MeasurableSet X) : ∫⁻ (x : α) in X, ‖f x‖ₑ ∂μ ≤ ∫⁻ (t : ENNReal) in Set.Iio (μ X), rearrangement f t μ

theorem MeasureTheory.setLIntegral_enorm_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : NullMeasurableSet X μ) : ∫⁻ (x : α) in X, ‖f x‖ₑ ∂μ = ∫⁻ (t : ENNReal), μ (X ∩ {x : α | t < ‖f x‖ₑ})

theorem MeasureTheory.setLIntegral_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {X : Set α} (hX : NullMeasurableSet X μ) : ∫⁻ (x : α) in X, f x ∂μ = ∫⁻ (t : ENNReal), μ (X ∩ {x : α | t < f x})

theorem MeasureTheory.lintegral_rearrangement_eq' {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} {t : ENNReal} : ∫⁻ (s : ENNReal) in Set.Iio t, rearrangement f s μ = ∫⁻ (s : ENNReal), min (distribution f s μ) t

theorem MeasureTheory.lintegral_rearrangement_eq'' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {t : ENNReal} : ∫⁻ (s : ENNReal) in Set.Iio (distribution f t μ), rearrangement f s μ = ∫⁻ (x : α) in {y : α | t < ‖f y‖ₑ}, ‖f x‖ₑ ∂μ

theorem MeasureTheory.lintegral_rearrangement_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ContinuousENorm ε] [NoAtoms' μ] {f : α → ε} (hf : AEStronglyMeasurable f μ) {t : ENNReal} : ∫⁻ (s : ENNReal) in Set.Iio t, rearrangement f s μ = ⨆ (E : Set α), ⨆ (_ : NullMeasurableSet E μ), ⨆ (_ : μ E ≤ t), ∫⁻ (x : α) in E, ‖f x‖ₑ ∂μ

theorem MeasureTheory.lintegral_rearrangement_eq_and {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ContinuousENorm ε] [NoAtoms' μ] {f : α → ε} (hf : AEStronglyMeasurable f μ) {t : ENNReal} : ∫⁻ (s : ENNReal) in Set.Iio t, rearrangement f s μ = ⨆ (E : Set α), ⨆ (_ : NullMeasurableSet E μ ∧ μ E ≤ t), ∫⁻ (x : α) in E, ‖f x‖ₑ ∂μ

theorem MeasureTheory.Antitone.lintegral_withDensity_le {f d : ENNReal → ENNReal} (hf : Antitone f) (hf' : AEMeasurable f volume) (hd : d ≤ 1) (hd' : AEMeasurable d volume) : ∫⁻ (t : ENNReal), f t ∂volume.withDensity d ≤ ∫⁻ (t : ENNReal) in Set.Iio (∫⁻ (t : ENNReal), d t), f t

theorem MeasureTheory.lintegral_rearrangement_add_rearrangement_le_add_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [ContinuousAdd ε] {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) {t : ENNReal} : ∫⁻ (s : ENNReal) in Set.Iio t, rearrangement (f + g) s μ ≤ (∫⁻ (s : ENNReal) in Set.Iio t, rearrangement f s μ) + ∫⁻ (s : ENNReal) in Set.Iio t, rearrangement g s μ