Decreasing rearrangements f^# #
noncomputable def
MeasureTheory.rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(t : ENNReal)
(μ : Measure α)
:
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}
Instances For
@[simp]
theorem
MeasureTheory.rearrangement_top
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.rearrangement_eq_zero_of_ae_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
(h : f =ᶠ[ae μ] 0)
:
@[simp]
theorem
MeasureTheory.rearrangement_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
:
theorem
MeasureTheory.rearrangement_antitone'
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{x y : ENNReal}
(h : x ≤ y)
:
theorem
MeasureTheory.rearrangement_antitone
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
Antitone fun (t : ENNReal) => rearrangement f t μ
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 ν)
:
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}
:
theorem
MeasureTheory.distribution_rearrangement_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{x : ENNReal}
:
theorem
MeasureTheory.lt_rearrangement_iff_lt_distribution
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{t y : ENNReal}
:
theorem
MeasureTheory.rearrangement_le_iff_distribution_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{t y : ENNReal}
:
@[simp]
theorem
MeasureTheory.distribution_rearrangement_eq_distribution
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{t : ENNReal}
:
@[simp]
theorem
MeasureTheory.support_rearrangement_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{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 μ) =ᶠ[ae volume] 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 ν]
:
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}
:
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 μ ≠ ⊤)
:
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)
:
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)
:
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 μ < ⊤)
:
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} = ⊤)
:
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 μ < ⊤)
:
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)
:
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)
:
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)
:
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)
:
theorem
MeasureTheory.lintegral_rearrangement_pow
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.lintegral_rearrangement
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.rearrangement_add_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x y : ENNReal}
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f g : α → ε}
:
theorem
MeasureTheory.sSup_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.rearrangement_zero_eq_eLpNormEssSup
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.eLpNorm'_rearrangement
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < 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)
:
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 μ)
:
theorem
MeasureTheory.lintegral_rearrangement_eq'
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
{t : ENNReal}
:
theorem
MeasureTheory.lintegral_rearrangement_eq''
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{t : ENNReal}
:
theorem
MeasureTheory.lintegral_rearrangement_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
[NoAtoms' μ]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{t : ENNReal}
:
theorem
MeasureTheory.lintegral_rearrangement_eq_and
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
[NoAtoms' μ]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{t : ENNReal}
:
theorem
MeasureTheory.lintegral_rearrangement_add_rearrangement_le_add_lintegral
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[ContinuousAdd ε]
{f g : α → ε}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
{t : ENNReal}
: