Decreasing rearrangements f^# #
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
theorem
MeasureTheory.rearrangement_mono_right
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{x y : ENNReal}
(h : x ≤ y)
:
theorem
MeasureTheory.rearrangement_mono_right'
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
Antitone fun (t : ENNReal) => rearrangement f 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}
:
theorem
MeasureTheory.distribution_rearrangement_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{x : ENNReal}
:
theorem
MeasureTheory.lt_rearrangement_iff
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{t y : ENNReal}
:
theorem
MeasureTheory.distribution_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{t : NNReal}
:
theorem
MeasureTheory.rearrangement_add_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x y : ENNReal}
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f g : α → ε}
:
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.volume_lt_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
[TopologicalSpace ε]
(hf : AEStronglyMeasurable f μ)
(s : ENNReal)
:
theorem
MeasureTheory.lintegral_rearrangement_pow
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
[TopologicalSpace ε]
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 1 ≤ p)
:
theorem
MeasureTheory.sSup_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.essSup_nnnorm_eq_rearrangement_zero
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
@[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.Ico 0 (μ s)).indicator (Function.const ENNReal ‖a‖ₑ) x
theorem
MeasureTheory.tendsto_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
[TopologicalSpace ε]
{s : ℕ → α → ε}
(hs : ∀ᶠ (i : ℕ) in Filter.atTop, AEStronglyMeasurable (s i) μ)
(hf : AEStronglyMeasurable f μ)
(h2s : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => ‖s n x‖ₑ)
(h : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => ‖s x_1 x‖ₑ) Filter.atTop (nhds ‖f x‖ₑ))
:
Filter.Tendsto s Filter.atTop (nhds f)
theorem
MeasureTheory.liminf_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
{x : ENNReal}
[TopologicalSpace ε]
{s : ℕ → α → ε}
(hs : ∀ᶠ (i : ℕ) in Filter.atTop, AEStronglyMeasurable (s i) μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ Filter.liminf (fun (x_1 : ℕ) => ‖s x_1 x‖ₑ) Filter.atTop)
:
theorem
MeasureTheory.distribution_indicator_le_distribution
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
[Zero ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ✝ : Measure α)
:
theorem
MeasureTheory.distribution_indicator_le_measure
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
[Zero ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ✝ : Measure α)
:
theorem
MeasureTheory.rearrangement_indicator_le'
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
[Zero ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ✝ : Measure α)
:
rearrangement (X.indicator f) t μ✝ ≤ (Set.Iio (μ✝ X)).indicator (fun (x : ENNReal) => rearrangement f x μ✝) t
Version of rearrangement_indicator_le for t : ℝ≥0∞
theorem
MeasureTheory.integral_norm_le_integral_rearrangement
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{X : Set α}
(hX : MeasurableSet X)
:
theorem
MeasureTheory.lintegral_rearrangement_eq
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
[NoAtoms μ]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{t : NNReal}
:
theorem
MeasureTheory.lintegral_rearrangement_add_rearrangement_le_add_lintegral
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[NoAtoms μ]
{f g : α → ε}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
{t : NNReal}
: