def MeasureTheory.superlevelSet {α : Type u_1} {ε : Type u_3} [ENorm ε] (f : α → ε) (t : ENNReal) : Set α

The superlevel set of a function f.

Equations

• MeasureTheory.superlevelSet f t = {x : α | t < ‖f x‖ₑ}

theorem MeasureTheory.superlevelSet_antitone {α : Type u_1} {ε : Type u_3} [ENorm ε] {f : α → ε} : Antitone (superlevelSet f)

theorem MeasureTheory.superlevelSet_zero_eq_support {α : Type u_1} {ε : Type u_12} [TopologicalSpace ε] [ENormedAddCommMonoid ε] {f : α → ε} : superlevelSet f 0 = Function.support f

theorem MeasureTheory.nullMeasurableSet_superlevelSet {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_12} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : NullMeasurableSet (superlevelSet f t) μ

theorem MeasureTheory.measurableSet_superlevelSet {α : Type u_1} {m : MeasurableSpace α} {t : ENNReal} {ε : Type u_12} [TopologicalSpace ε] [ContinuousENorm ε] [MeasurableSpace ε] [OpensMeasurableSpace ε] {f : α → ε} (hf : Measurable f) : MeasurableSet (superlevelSet f t)

theorem MeasureTheory.superlevelSet_const {α : Type u_1} {ε : Type u_3} {t : ENNReal} [ENorm ε] {a : ε} : superlevelSet (Function.const α a) t = if t < ‖a‖ₑ then Set.univ else ∅

The distribution function d_f

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

The distribution function of a function f. Todo: rename to something more Mathlib-appropriate.

Equations

• MeasureTheory.distribution f t μ = μ {x : α | t < ‖f x‖ₑ}

theorem MeasureTheory.distribution_eq_measure_superlevelSet {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} [ENorm ε] {f : α → ε} : distribution f t μ = μ (superlevelSet f t)

@[simp]

theorem MeasureTheory.distibution_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [ENorm ε] (f : α → ε) (μ : Measure α) : distribution f ⊤ μ = 0

theorem MeasureTheory.distribution_mono_right {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t s : ENNReal} [ENorm ε] {f : α → ε} (h : t ≤ s) : distribution f s μ ≤ distribution f t μ

theorem MeasureTheory.distribution_mono_right' {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} : Antitone fun (t : ENNReal) => distribution f t μ

theorem MeasureTheory.distribution_congr_ae {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} [ENorm ε] {f g : α → ε} (h : ∀ᵐ (x : α) ∂μ, f x = g x) : distribution f t μ = distribution g t μ

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

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

theorem MeasureTheory.distribution_toReal_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → ENNReal} : distribution (ENNReal.toReal ∘ f) t μ ≤ distribution f t μ

theorem MeasureTheory.distribution_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : distribution (ENNReal.toReal ∘ f) t μ = distribution f t μ

theorem MeasureTheory.distribution_add_le_of_enorm {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t s : ENNReal} [ENorm ε] {f g₁ g₂ : α → ε} {A : ENNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ)) : distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ

theorem MeasureTheory.approx_above_superset {α : Type u_1} {ε : Type u_3} [ENorm ε] {f : α → ε} (t₀ : ENNReal) : ⋃ (n : ℕ), (fun (n : ℕ) => {x : α | t₀ + (↑n)⁻¹ < ‖f x‖ₑ}) n = {x : α | t₀ < ‖f x‖ₑ}

theorem MeasureTheory.tendsto_measure_iUnion_distribution {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (t₀ : ENNReal) : Filter.Tendsto (⇑μ ∘ fun (n : ℕ) => {x : α | t₀ + (↑n)⁻¹ < ‖f x‖ₑ}) Filter.atTop (nhds (μ {x : α | t₀ < ‖f x‖ₑ}))

theorem MeasureTheory.select_neighborhood_distribution {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (t₀ l : ENNReal) (hu : l < distribution f t₀ μ) : ∃ (n : ℕ), l < distribution f (t₀ + (↑n)⁻¹) μ

theorem MeasureTheory.continuousWithinAt_distribution {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (t₀ : ENNReal) : ContinuousWithinAt (fun (x : ENNReal) => distribution f x μ) (Set.Ioi t₀) t₀

theorem MeasureTheory.distribution_pow {α : Type u_1} {m : MeasurableSpace α} (ε : Type u_12) [SeminormedRing ε] [NormOneClass ε] [NormMulClass ε] (f : α → ε) (t : ENNReal) (μ : Measure α) {n : ℕ} (hn : n ≠ 0) : distribution (f ^ n) (t ^ n) μ = distribution f t μ

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

theorem MeasureTheory.distribution_mono {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t s : ENNReal} [ENorm ε] {ε' : Type u_12} [ENorm ε'] {f : α → ε} {g : α → ε'} (h₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) (h₂ : t ≤ s) : distribution f s μ ≤ distribution g t μ

theorem MeasureTheory.distribution_eLpNormEssSup {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} : distribution f (eLpNormEssSup f μ) μ = 0

theorem MeasureTheory.distribution_add_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t s : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f g : α → ε} : distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ

theorem MeasureTheory.distribution_eq_zero_of_ae_zero_enorm {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} [ENorm ε] {f : α → ε} (h : enorm ∘ f =ᵐ[μ] 0) : distribution f t μ = 0

theorem MeasureTheory.distribution_eq_zero_of_ae_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : f =ᵐ[μ] 0) : distribution f t μ = 0

@[simp]

theorem MeasureTheory.distribution_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ENormedAddMonoid ε] : distribution 0 t μ = 0

theorem MeasureTheory.distribution_zero_eq_measure_support {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_13} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} : distribution f 0 μ = μ (Function.support f)

theorem MeasureTheory.distribution_indicator_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {X : Set α} : distribution (X.indicator f) x μ = μ (X ∩ superlevelSet f x)

theorem MeasureTheory.distribution_indicator_le_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {X : Set α} : distribution (X.indicator f) x μ ≤ μ X

theorem MeasureTheory.distribution_indicator_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {a : ε} : distribution (s.indicator (Function.const α a)) t μ = (Set.Iio ‖a‖ₑ).indicator (fun (x : ENNReal) => μ s) t

theorem MeasureTheory.distribution_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {a : ε} : distribution (Function.const α a) t μ = (Set.Iio ‖a‖ₑ).indicator (fun (x : ENNReal) => μ Set.univ) t

theorem MeasureTheory.distribution_indicator_superlevelSet {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {x : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} {t : ENNReal} : distribution ((superlevelSet f t).indicator f) x μ = min (distribution f t μ) (distribution f x μ)

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

theorem MeasureTheory.distribution_eq_zero_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} : distribution f t μ = 0 ↔ eLpNormEssSup f μ ≤ t

theorem MeasureTheory.support_distribution {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} : (Function.support fun (t : ENNReal) => distribution f t μ) = Set.Iio (eLpNormEssSup f μ)

theorem MeasureTheory.distribution_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f g : α → ε} (h : Disjoint (Function.support f) (Function.support g)) (hg : AEStronglyMeasurable g μ) : distribution (f + g) t μ = distribution f t μ + distribution g t μ

theorem MeasureTheory.distribution_const_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → ENNReal} {a : ENNReal} (h : a ≠ 0 ∨ t ≠ 0) (h' : a ≠ ⊤ ∨ t ≠ ⊤) : distribution (a • f) t μ = distribution f (t / a) μ

theorem MeasureTheory.distribution_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → ENNReal} {a : ENNReal} (h : a ≠ ⊤ ∨ t ≠ 0) (h' : a ≠ 0 ∨ t ≠ ⊤) : distribution f (a * t) μ = distribution (fun (x : α) => f x / a) t μ

theorem MeasureTheory.distribution_indicator_add_of_support_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε : Type u_13} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (enorm_add : ∀ (a b : ε), ‖a + b‖ₑ = ‖a‖ₑ + ‖b‖ₑ) {f : α → ε} {c : ε} (hc : ‖c‖ₑ ≠ ⊤) {s : Set α} (hfs : Function.support f ⊆ s) : distribution (f + s.indicator (Function.const α c)) t μ = if t < ‖c‖ₑ then μ s else distribution f (t - ‖c‖ₑ) μ

theorem MeasureTheory.distribution_indicator_add_of_support_subset_ennreal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) {s : Set α} (hfs : Function.support f ⊆ s) : distribution (f + s.indicator (Function.const α c)) t μ = if t < c then μ s else distribution f (t - c) μ

theorem MeasureTheory.distribution_indicator_add_of_support_subset_nnreal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {f : α → NNReal} {c : NNReal} {s : Set α} (hfs : Function.support f ⊆ s) : distribution (f + s.indicator (Function.const α c)) t μ = if t < ↑c then μ s else distribution f (t - ↑c) μ

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

theorem MeasureTheory.distribution_le_mul_pow_eLpNorm_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_13} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε'} {ε : ENNReal} (hε : ε ≠ 0) (hmeas_top : ε = ⊤ → μ {x : α | ‖f x‖ₑ = ⊤} = 0) : distribution f ε μ ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

noncomputable def MeasureTheory.C_distribution_le_of_eLpNorm_le (δ ε p : NNReal) : NNReal

The constant used in C_distribution_le_of_eLpNorm_le.

Equations

• MeasureTheory.C_distribution_le_of_eLpNorm_le δ ε p = δ * ε ^ (↑p)⁻¹

theorem MeasureTheory.C_distribution_le_of_eLpNorm_le_pos {δ ε p : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_distribution_le_of_eLpNorm_le δ ε p

theorem MeasureTheory.distribution_le_of_eLpNorm_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_13} [TopologicalSpace ε'] [ContinuousENorm ε'] {δ ε p : NNReal} (δpos : 0 < δ) (p_pos : 0 < p) {f : α → ε'} (hf : eLpNorm f (↑p) μ ≤ ↑(C_distribution_le_of_eLpNorm_le δ ε p)) : distribution f (↑δ) μ ≤ ↑ε

theorem MeasureTheory.distribution_lt_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : MemLp f p μ) (p_pos : 0 < p) (p_ne_top : p ≠ ⊤) {t : NNReal} (ht : 0 < t) : distribution f (↑t) μ < ⊤

A function in L^p for 0 < p < ∞ has finite distribution function at every t > 0, by the Chebyshev–Markov inequality.

theorem MeasureTheory.distribution_le {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} [MeasurableSpace ε] [OpensMeasurableSpace ε] {c : ENNReal} (hc : c ≠ 0) {μ : Measure α} (hf : AEMeasurable f μ) : distribution f c μ ≤ c⁻¹ * ∫⁻ (y : α), ‖f y‖ₑ ∂μ

theorem MeasureTheory.distribution_smul_left {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : ENNReal} {ε' : Type u_12} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [SMul NNReal ε'] [ENormSMulClass NNReal ε'] {f : α → ε'} {c : NNReal} (hc : c ≠ 0) : distribution (c • f) t μ = distribution f (t / ‖c‖ₑ) μ

theorem MeasureTheory.distribution_smul_left' {α : Type u_1} {𝕜 : Type u_7} {E : Type u_8} {m : MeasurableSpace α} {μ : Measure α} [NontriviallyNormedField 𝕜] {t : ENNReal} [NormedAddCommGroup E] [MulActionWithZero 𝕜 E] [NormSMulClass 𝕜 E] {f : α → E} {c : 𝕜} (hc : c ≠ 0) : distribution (c • f) t μ = distribution f (t / ‖c‖ₑ) μ

theorem ContinuousLinearMap.distribution_le {α : Type u_1} {𝕜 : Type u_7} {E₁ : Type u_9} {E₂ : Type u_10} {E₃ : Type u_11} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NontriviallyNormedField 𝕜] {t s : ENNReal} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {f : α → E₁} {g : α → E₂} (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) : MeasureTheory.distribution (fun (x : α) => (L (f x)) (g x)) (‖L‖ₑ * t * s) μ ≤ MeasureTheory.distribution f t μ + MeasureTheory.distribution g s μ