def
MeasureTheory.eLorentzNorm'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p r : ENNReal)
(μ : Measure α)
:
The Lorentz norm of a function, for p < ∞
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.eLorentzNorm
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p r : ENNReal)
(μ : Measure α)
:
The Lorentz norm of a function
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MeasureTheory.eLorentzNorm_eq_eLorentzNorm'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{p r : ENNReal}
{μ : Measure α}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
@[simp]
theorem
MeasureTheory.eLorentzNorm_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{p r : ENNReal}
{μ : Measure α}
(hp : p = 0)
:
@[simp]
theorem
MeasureTheory.eLorentzNorm_zero'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{p r : ENNReal}
{μ : Measure α}
(hr : r = 0)
:
theorem
MeasureTheory.eLorentzNorm_zero_of_ae_zero
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p r : ENNReal}
{μ : Measure α}
{f : α → ε'}
(h : f =ᶠ[ae μ] 0)
:
theorem
MeasureTheory.eLorentzNorm'_mono
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p r : ENNReal}
{μ : Measure α}
{f g : α → ε'}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
:
theorem
MeasureTheory.eLorentzNorm_mono
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p r : ENNReal}
{μ : Measure α}
{f g : α → ε'}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
:
@[simp]
theorem
MeasureTheory.eLorentzNorm_top_top
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
:
theorem
MeasureTheory.eLorentzNorm_eq_eLpNorm
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p : ENNReal}
{μ : Measure α}
{f : α → ε'}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.aeMeasurable_withDensity_inv
{f : NNReal → ENNReal}
(hf : AEMeasurable f volume)
:
AEMeasurable f (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)
theorem
MeasureTheory.essSup_le_iSup
{α : Type u_4}
{β : Type u_5}
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteLattice β]
(f : α → β)
:
theorem
MeasureTheory.ContinuousWithinAt.ennreal_mul
{X : Type u_4}
[TopologicalSpace X]
{f g : X → ENNReal}
{s : Set X}
{t : X}
(hf : ContinuousWithinAt f s t)
(hg : ContinuousWithinAt g s t)
(h₁ : f t ≠ 0 ∨ g t ≠ ⊤)
(h₂ : g t ≠ 0 ∨ f t ≠ ⊤)
:
ContinuousWithinAt (fun (x : X) => f x * g x) s t
theorem
MeasureTheory.ContinuousWithinAt.ennrpow_const
{α : Type u_1}
[TopologicalSpace α]
{f : α → ENNReal}
{s : Set α}
{x : α}
{p : ℝ}
(hf : ContinuousWithinAt f s x)
:
ContinuousWithinAt (fun (x : α) => f x ^ p) s x
theorem
MeasureTheory.eLorentzNorm_eq_wnorm
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{p : ENNReal}
{μ : Measure α}
(hp : p ≠ 0)
:
theorem
MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
{p : ENNReal}
{μ : Measure α}
:
theorem
MeasureTheory.eLorentzNorm'_indicator
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{a : ε}
(ha : ‖a‖ₑ ≠ ⊤)
{s : Set α}
(p_ne_zero : p ≠ 0)
(p_ne_top : p ≠ ⊤)
:
def
MeasureTheory.MemLorentz
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
[TopologicalSpace ε]
(f : α → ε)
(p r : ENNReal)
(μ : Measure α)
:
A function is in the Lorentz space L_{pr} if it is (strongly a.e.)-measurable and has finite Lorentz norm.
Equations
- MeasureTheory.MemLorentz f p r μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLorentzNorm f p r μ < ⊤)
Instances For
theorem
MeasureTheory.MemLorentz_iff_MemLp
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p : ENNReal}
{μ : Measure α}
{f : α → ε'}
:
theorem
MeasureTheory.MemLorentz_of_MemLorentz_ge
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_4}
[ENorm ε]
[TopologicalSpace ε]
{f : α → ε}
{p r₁ r₂ : ENNReal}
{μ : Measure α}
(r₁_pos : 0 < r₁)
(r₁_le_r₂ : r₁ ≤ r₂)
(hf : MemLorentz f p r₁ μ)
:
MemLorentz f p r₂ μ
theorem
MeasureTheory.MemLorentz.memLp
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
{p r : ENNReal}
{μ : Measure α}
{f : α → ε'}
(hf : MemLorentz f p r μ)
(h : r ∈ Set.Ioc 0 p)
:
MemLp f p μ
def
MeasureTheory.HasLorentzType
{α : Type u_1}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{ε₁ : Type u_5}
{ε₂ : Type u_6}
{m : MeasurableSpace α'}
[TopologicalSpace ε₁]
[ENorm ε₁]
[TopologicalSpace ε₂]
[ENorm ε₂]
(T : (α → ε₁) → α' → ε₂)
(p r q s : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An operator has Lorentz type (p, r, q, s) if it is bounded as a map
from L^{q, s} to L^{p, r}. HasLorentzType T p r q s μ ν c means that
T has Lorentz type (p, r, q, s) w.r.t. measures μ, ν and constant c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.hasStrongType_iff_hasLorentzType
{α : Type u_1}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{m : MeasurableSpace α'}
{ε₁ : Type u_7}
{ε₂ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENormedAddMonoid ε₂]
{T : (α → ε₁) → α' → ε₂}
{p q : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{c : ENNReal}
:
def
MeasureTheory.HasRestrictedWeakType
{α : Type u_1}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{ε₂ : Type u_6}
{m : MeasurableSpace α'}
[TopologicalSpace ε₂]
[ENorm ε₂]
{β : Type u_7}
[Zero β]
[One β]
(T : (α → β) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
Defines when an operator "has restricted weak type". This is an even weaker version
of HasBoundedWeakType.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.HasRestrictedWeakType.without_finiteness
{α : Type u_1}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{m : MeasurableSpace α'}
{β : Type u_7}
[Zero β]
[One β]
{ε₂ : Type u_8}
[TopologicalSpace ε₂]
[ENormedAddMonoid ε₂]
{T : (α → β) → α' → ε₂}
{p p' : ENNReal}
(p_ne_zero : p ≠ 0)
(p_ne_top : p ≠ ⊤)
(p'_ne_zero : p' ≠ 0)
(p'_ne_top : p' ≠ ⊤)
{μ : Measure α}
{ν : Measure α'}
{c : NNReal}
(c_pos : 0 < c)
(hT : HasRestrictedWeakType T p p' μ ν ↑c)
(F : Set α)
(G : Set α')
:
theorem
MeasureTheory.Filter.mono_limsup
{α : Type u_8}
{β : Type u_9}
[CompleteLattice α]
{f : Filter β}
{u v : β → α}
(h : ∀ (x : β), u x ≤ v x)
:
theorem
MeasureTheory.Filter.limsup_le_of_le'
{α : Type u_8}
{β : Type u_9}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
{a : α}
(h : ∀ᶠ (n : β) in f, u n ≤ a)
:
def
MeasureTheory.WeaklyContinuous
{α : Type u_1}
{ε : Type u_2}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{m : MeasurableSpace α'}
[TopologicalSpace ε]
[ENorm ε]
[ENorm ε']
[SupSet ε]
[Preorder ε]
(T : (α → ε) → α' → ε')
(p : ENNReal)
(μ : Measure α)
(ν : Measure α')
:
The weak continuity assumption neede for HasRestrictedWeakType.hasLorentzType_helper.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.HasRestrictedWeakType.hasLorentzType_helper
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{m : MeasurableSpace α'}
[TopologicalSpace ε']
[ENormedSpace ε']
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{c : NNReal}
(c_pos : 0 < c)
{T : (α → NNReal) → α' → ε'}
(hT : HasRestrictedWeakType T p p' μ ν ↑c)
(hpp' : p.HolderConjugate p')
(weakly_cont_T : WeaklyContinuous T p μ ν)
{G : Set α'}
(hG : MeasurableSet G)
(hG' : ν G < ⊤)
(T_subadditive :
∀ (f g : α → NNReal),
MemLorentz f p 1 μ →
MemLorentz g p 1 μ →
eLpNorm (T (f + g)) 1 (ν.restrict G) ≤ eLpNorm (T f) 1 (ν.restrict G) + eLpNorm (T g) 1 (ν.restrict G))
(T_submult : ∀ (f : α → NNReal) (a : NNReal), eLpNorm (T (a • f)) 1 (ν.restrict G) ≤ eLpNorm (a • T f) 1 (ν.restrict G))
{f : α → NNReal}
(hf : Measurable f)
(hf' : MemLorentz f p 1 μ)
:
theorem
MeasureTheory.HasRestrictedWeakType.hasLorentzType
{α : Type u_1}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
{α' : Type u_4}
{m : MeasurableSpace α'}
[TopologicalSpace α]
{𝕂 : Type u_8}
[RCLike 𝕂]
[TopologicalSpace ε']
[ENormedSpace ε']
{T : (α → 𝕂) → α' → ε'}
{p p' : ENNReal}
{μ : Measure α}
[IsLocallyFiniteMeasure μ]
{ν : Measure α'}
{c : NNReal}
(c_pos : 0 < c)
(hT : HasRestrictedWeakType T p p' μ ν ↑c)
(hpp' : p.HolderConjugate p')
(T_meas : ∀ {f : α → 𝕂}, MemLorentz f p 1 μ → AEStronglyMeasurable (T f) ν)
(T_subadd : ∀ (f g : α → 𝕂) (x : α'), MemLorentz f p 1 μ → MemLorentz g p 1 μ → ‖T (f + g) x‖ₑ ≤ ‖T f x + T g x‖ₑ)
(T_submul : ∀ (a : 𝕂) (f : α → 𝕂) (x : α'), ‖T (a • f) x‖ₑ ≤ ‖a‖ₑ • ‖T f x‖ₑ)
(weakly_cont_T :
∀ {f : α → 𝕂} {fs : ℕ → α → 𝕂},
LocallyIntegrable f μ →
(∀ (n : ℕ), AEStronglyMeasurable (fs n) μ) →
(∀ (a : α), Monotone fun (n : ℕ) => ‖fs n a‖) →
(∀ (a : α), Filter.Tendsto (fun (n : ℕ) => fs n a) Filter.atTop (nhds (f a))) →
∀ (G : Set α'),
eLpNorm (T f) 1 (ν.restrict G) ≤ Filter.limsup (fun (n : ℕ) => eLpNorm (T (fs n)) 1 (ν.restrict G)) Filter.atTop)
:
HasLorentzType T p 1 p ⊤ μ ν (4 * ↑c / p)