The distribution function d_f #
def
MeasureTheory.distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(t : ENNReal)
(μ : Measure α)
:
The distribution function of a function f.
Todo: rename to something more Mathlib-appropriate.
Instances For
@[simp]
theorem
MeasureTheory.distibution_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(μ : Measure α)
:
theorem
MeasureTheory.distribution_mono_right
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
[ENorm ε]
{f : α → ε}
(h : t ≤ s)
:
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_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}
:
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)
:
def
MeasureTheory.wnorm'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p : ℝ)
(μ : Measure α)
:
The weak L^p norm of a function, for p < ∞
Equations
- MeasureTheory.wnorm' f p μ = ⨆ (t : NNReal), ↑t * MeasureTheory.distribution f (↑t) μ ^ p⁻¹
Instances For
theorem
MeasureTheory.wnorm'_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(μ : Measure α)
:
theorem
MeasureTheory.wnorm'_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ℝ}
(hp : 0 ≤ p)
:
def
MeasureTheory.wnorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
The weak L^p norm of a function.
Equations
- MeasureTheory.wnorm f p μ = if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.wnorm' f p.toReal μ
Instances For
@[simp]
theorem
MeasureTheory.wnorm_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.wnorm_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
theorem
MeasureTheory.wnorm_ofReal
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
{p : ℝ}
(hp : 0 ≤ p)
:
theorem
MeasureTheory.wnorm_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ENNReal}
:
def
MeasureTheory.MemWLp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
[TopologicalSpace ε]
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm.
Equations
- MeasureTheory.MemWLp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.wnorm f p μ < ⊤)
Instances For
theorem
MeasureTheory.MemWLp_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
:
theorem
MeasureTheory.MemWLp.aeStronglyMeasurable
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
(hf : MemWLp f p μ)
:
theorem
MeasureTheory.MemWLp.wnorm_lt_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
(hf : MemWLp f p μ)
:
theorem
MeasureTheory.MemWLp.ennreal_toReal
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{f : α → ENNReal}
(hf : MemWLp f p μ)
:
MemWLp (ENNReal.toReal ∘ f) p μ
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 μ)
:
theorem
MeasureTheory.wnorm'_le_eLpNorm'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(p0 : 0 < p)
:
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)
:
theorem
MeasureTheory.wnorm_le_eLpNorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ENNReal}
(hp : 0 < p)
:
theorem
MeasureTheory.MemLp.memWLp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hp : 0 < p)
(hf : MemLp f p μ)
:
MemWLp f p μ
def
MeasureTheory.HasWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q.
HasWeakType T p p' μ ν c means that T has weak type (p, p') w.r.t. measures μ, ν
and constant c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasBoundedWeakType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
A weaker version of HasWeakType.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasStrongType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q.
HasStrongType T p p' μ ν c means that T has strong type (p, p') w.r.t. measures μ, ν
and constant c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasBoundedStrongType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
A weaker version of HasStrongType. This is the same as HasStrongType if T is continuous
w.r.t. the L^2 norm, but weaker in general.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lemmas about HasWeakType #
theorem
MeasureTheory.HasWeakType.memWLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasWeakType T p p' μ ν c)
(hf₁ : MemLp f₁ p μ)
(hc : c < ⊤ := by finiteness)
:
MemWLp (T f₁) p' ν
theorem
MeasureTheory.HasWeakType.toReal
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasWeakType T p p' μ ν c)
:
HasWeakType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c
theorem
MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : NullMeasurableSet (f ⁻¹' {⊤}) μ)
:
theorem
MeasureTheory.hasWeakType_toReal_iff
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), MemLp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
Lemmas about HasBoundedWeakType #
theorem
MeasureTheory.HasBoundedWeakType.memWLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENorm ε₂]
{f₁ : α → ε₁}
(h : HasBoundedWeakType T p p' μ ν c)
(hf₁ : BoundedFiniteSupport f₁ μ)
(hc : c < ⊤ := by finiteness)
:
MemWLp (T f₁) p' ν
theorem
MeasureTheory.HasWeakType.hasBoundedWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENorm ε₂]
(h : HasWeakType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
Lemmas about HasStrongType #
theorem
MeasureTheory.HasStrongType.memLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasStrongType T p p' μ ν c)
(hf₁ : MemLp f₁ p μ)
(hc : c < ⊤ := by finiteness)
:
MemLp (T f₁) p' ν
theorem
MeasureTheory.HasStrongType.hasWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(hp' : 0 < p')
(h : HasStrongType T p p' μ ν c)
:
HasWeakType T p p' μ ν c
theorem
MeasureTheory.HasStrongType.toReal
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasStrongType T p p' μ ν c)
:
HasStrongType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c
theorem
MeasureTheory.hasStrongType_toReal_iff
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), MemLp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
HasStrongType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c ↔ HasStrongType T p p' μ ν c
Lemmas about HasBoundedStrongType #
theorem
MeasureTheory.HasBoundedStrongType.memLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasBoundedStrongType T p p' μ ν c)
(hf₁ : BoundedFiniteSupport f₁ μ)
(hc : c < ⊤ := by finiteness)
:
MemLp (T f₁) p' ν
theorem
MeasureTheory.HasStrongType.hasBoundedStrongType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(h : HasStrongType T p p' μ ν c)
:
HasBoundedStrongType T p p' μ ν c
theorem
MeasureTheory.HasBoundedStrongType.hasBoundedWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(hp' : 0 < p')
(h : HasBoundedStrongType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
theorem
MeasureTheory.HasBoundedStrongType.const_smul
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasBoundedStrongType T p p' μ ν c)
(r : NNReal)
:
HasBoundedStrongType (r • T) p p' μ ν (r • c)
theorem
MeasureTheory.distribution_snormEssSup
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[ENorm ε]
:
theorem
MeasureTheory.distribution_add_le
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f g : α → ε}
:
theorem
MeasureTheory.distribution_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(h : f =ᶠ[ae μ] 0)
:
theorem
MeasureTheory.distribution_indicator_const
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{s : Set α}
{a : ε}
:
distribution (s.indicator (Function.const α a)) t μ = (Set.Iio ‖a‖ₑ).indicator (fun (x : ENNReal) => μ s) t
theorem
MeasureTheory.distribution_add
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f g : α → ε}
(h : Disjoint (Function.support f) (Function.support g))
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.distribution_indicator_add_of_support_subset
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
(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_smul_left
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε' : Type u_13}
[TopologicalSpace ε']
[ENormedSpace ε']
{f : α → ε'}
{c : NNReal}
(hc : c ≠ 0)
:
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)
:
theorem
MeasureTheory.HasStrongType.const_smul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
{ε' : Type u_13}
[TopologicalSpace ε]
[ENorm ε]
[TopologicalSpace ε']
[ENormedSpace ε']
[ContinuousConstSMul NNReal ε']
{T : (α → ε) → α' → ε'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(k : NNReal)
:
HasStrongType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_smul'
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{𝕜 : Type u_15}
{E' : Type u_16}
[NormedRing 𝕜]
[NormedAddCommGroup E']
[MulActionWithZero 𝕜 E']
[IsBoundedSMul 𝕜 E']
{T : (α → ε) → α' → E'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(k : 𝕜)
:
HasStrongType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_mul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → ENNReal}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(e : NNReal)
:
HasStrongType (fun (f : α → ε) (x : α') => ↑e * T f x) p p' μ ν (‖e‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_mul'
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{E' : Type u_15}
[NormedRing E']
{T : (α → ε) → α' → E'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(e : E')
:
HasStrongType (fun (f : α → ε) (x : α') => e * T f x) p p' μ ν (‖e‖ₑ * c)
theorem
MeasureTheory.wnorm_const_smul_le
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε' : Type u_13}
[TopologicalSpace ε']
[ENormedSpace ε']
(hp : p ≠ 0)
{f : α → ε'}
(k : NNReal)
:
theorem
MeasureTheory.wnorm_const_smul_le'
{α : Type u_1}
{𝕜 : Type u_7}
{E : Type u_8}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[NormSMulClass 𝕜 E]
[IsBoundedSMul 𝕜 E]
(hp : p ≠ 0)
{f : α → E}
(k : 𝕜)
:
theorem
MeasureTheory.HasWeakType.const_smul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
{ε' : Type u_13}
[TopologicalSpace ε]
[ENorm ε]
[TopologicalSpace ε']
[ENormedSpace ε']
[ContinuousConstSMul NNReal ε']
{T : (α → ε) → α' → ε'}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(k : NNReal)
:
HasWeakType (k • T) p p' μ ν (↑k * c)
theorem
MeasureTheory.HasWeakType.const_smul'
{α : Type u_1}
{α' : Type u_2}
{𝕜 : Type u_7}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[NontriviallyNormedField 𝕜]
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{E' : Type u_14}
[NormedAddCommGroup E']
[MulActionWithZero 𝕜 E']
[NormSMulClass 𝕜 E']
[IsBoundedSMul 𝕜 E']
{T : (α → ε) → α' → E'}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(k : 𝕜)
:
HasWeakType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasWeakType.const_mul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → ENNReal}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(e : NNReal)
:
HasWeakType (fun (f : α → ε) (x : α') => ↑e * T f x) p p' μ ν (↑e * c)
theorem
MeasureTheory.HasWeakType.const_mul'
{α : Type u_1}
{α' : Type u_2}
{𝕜 : Type u_7}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[NontriviallyNormedField 𝕜]
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → 𝕜}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(e : 𝕜)
:
HasWeakType (fun (f : α → ε) (x : α') => e * T f x) p p' μ ν (‖e‖ₑ * 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 μ
theorem
MeasureTheory.lintegral_norm_pow_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
The layer-cake theorem, or Cavalieri's principle for functions into a space with a continuous enorm.
theorem
MeasureTheory.eLpNorm_pow_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : NNReal}
(hp : 0 < p)
:
eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (t : ℝ) in Set.Ioi 0, ↑p * ENNReal.ofReal (t ^ (↑p - 1)) * distribution f (ENNReal.ofReal t) μ
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm.
theorem
MeasureTheory.eLpNorm_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
eLpNorm f (ENNReal.ofReal p) μ = (ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, distribution f (ENNReal.ofReal t) μ * ENNReal.ofReal (t ^ (p - 1))) ^ p⁻¹
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without
taking powers.
theorem
MeasureTheory.lintegral_pow_mul_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : -1 < p)
: