def
MeasureTheory.HasLorentzType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_3}
{ε₂ : Type u_4}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
[ENorm ε₁]
[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}
{α' : Type u_2}
{ε₁ : Type u_3}
{ε₂ : Type u_4}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{p q : ENNReal}
[ESeminormedAddMonoid ε₁]
[ESeminormedAddMonoid ε₂]
{T : (α → ε₁) → α' → ε₂}
{c : ENNReal}
:
def
MeasureTheory.HasRestrictedWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₂ : Type u_4}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
[TopologicalSpace ε₂]
{β : Type u_5}
[Zero β]
[One β]
[ENorm ε₂]
(T : (α → β) → α' → ε₂)
(p q : 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}
{α' : Type u_2}
{ε₂ : Type u_4}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₂]
{p q : ENNReal}
{β : Type u_5}
[Zero β]
[One β]
[ESeminormedAddMonoid ε₂]
{T : (α → β) → α' → ε₂}
(p_ne_zero : p ≠ 0)
(p_ne_top : p ≠ ⊤)
(q_ne_zero : q ≠ 0)
(q_ne_top : q ≠ ⊤)
{c : NNReal}
(c_pos : 0 < c)
(hT : HasRestrictedWeakType T p q μ ν ↑c)
(T_zero_of_ae_zero : ∀ {f : α → β}, f =ᶠ[ae μ] 0 → enorm ∘ T f =ᶠ[ae ν] 0)
(F : Set α)
(G : Set α')
:
def
MeasureTheory.HasRestrictedWeakType'
{α : Type u_1}
{α' : Type u_2}
{ε₂ : Type u_4}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
[TopologicalSpace ε₂]
{β : Type u_5}
[TopologicalSpace β]
[ENorm β]
[ENorm ε₂]
(T : (α → β) → α' → ε₂)
(p q : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An enhanced version of HasRestrictedWeakType
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Filter.mono_limsup
{α : Type u_6}
{β : Type u_7}
[CompleteLattice α]
{f : Filter β}
{u v : β → α}
(h : ∀ (x : β), u x ≤ v x)
:
theorem
MeasureTheory.Filter.limsup_le_of_le'
{α : Type u_6}
{β : Type u_7}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
{a : α}
(h : ∀ᶠ (n : β) in f, u n ≤ a)
:
theorem
MeasureTheory.ENNReal.limsup_mul_const
{α : Type u_1}
{f : Filter α}
[CountableInterFilter f]
{u : α → ENNReal}
{a : ENNReal}
:
def
MeasureTheory.WeaklyContinuous
{α : Type u_1}
{α' : Type u_2}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{ε : Type u_6}
{ε' : Type u_7}
[TopologicalSpace ε]
[ENorm ε]
[SupSet ε]
[Preorder ε]
[ENorm ε']
(T : (α → ε) → α' → ε')
(p : ENNReal)
(μ : Measure α)
(ν : Measure α')
:
The weak continuity assumption needed for HasRestrictedWeakType.hasLorentzType_helper.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.HasRestrictedWeakType.hasRestrictedWeakType'_nnreal
{α : Type u_1}
{α' : Type u_2}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{p q : ENNReal}
{ε' : Type u_7}
[TopologicalSpace ε']
[ENormedSpace ε']
{c : NNReal}
(c_pos : 0 < c)
{T : (α → NNReal) → α' → ε'}
(p_ne_top : p ≠ ⊤)
(q_ne_top : q ≠ ⊤)
(hpq : p.HolderConjugate q)
(T_meas : ∀ {f : α → NNReal}, MemLorentz f p 1 μ → AEStronglyMeasurable (T f) ν)
(T_subadd :
∀ {f g : α → NNReal}, MemLorentz f p 1 μ → MemLorentz g p 1 μ → ∀ᵐ (x : α') ∂ν, ‖T (f + g) x‖ₑ ≤ ‖T f x‖ₑ + ‖T g x‖ₑ)
(T_submul : ∀ (a : NNReal) (f : α → NNReal), ∀ᵐ (x : α') ∂ν, ‖T (a • f) x‖ₑ ≤ ‖a‖ₑ * ‖T f x‖ₑ)
(T_ae_eq_of_ae_eq : ∀ {f g : α → NNReal}, f =ᶠ[ae μ] g → T f =ᶠ[ae ν] T g)
(T_zero : T 0 =ᶠ[ae ν] 0)
(hT : HasRestrictedWeakType T p q μ ν ↑c)
(weakly_cont_T : WeaklyContinuous T p μ ν)
:
HasRestrictedWeakType' T p q μ ν (↑c / p)
theorem
MeasureTheory.HasRestrictedWeakType'.hasLorentzType
{α : Type u_1}
{α' : Type u_2}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{p q : ENNReal}
{ε' : Type u_7}
[SigmaFinite ν]
{𝕂 : Type u_8}
[RCLike 𝕂]
[TopologicalSpace ε']
[ENormedSpace ε']
{T : (α → 𝕂) → α' → ε'}
(hpq : p.HolderConjugate q)
(hp : p ≠ ⊤)
(hq : q ≠ ⊤)
{c : ENNReal}
(hc : c ≠ ⊤)
(hT : HasRestrictedWeakType' T p q μ ν c)
:
HasLorentzType T p 1 p ⊤ μ ν c
theorem
MeasureTheory.RCLike.Components.norm_eq_one
{𝕂 : Type u_8}
[RCLike 𝕂]
{c : 𝕂}
(hc : c ∈ Components)
(hc' : c ≠ 0)
:
theorem
MeasureTheory.RCLike.Components.norm_le_one
{𝕂 : Type u_8}
[RCLike 𝕂]
{c : 𝕂}
(hc : c ∈ Components)
:
TODO: check whether this is the right approach
Equations
- MeasureTheory.RCLike.component c a = (RCLike.re (a * (starRingEnd 𝕂) c)).toNNReal
Instances For
theorem
MeasureTheory.RCLike.component_le_norm
{𝕂 : Type u_8}
[RCLike 𝕂]
{c a : 𝕂}
(hc : c ∈ Components)
:
theorem
MeasureTheory.RCLike.component_le_nnnorm
{𝕂 : Type u_8}
[RCLike 𝕂]
{c a : 𝕂}
(hc : c ∈ Components)
:
theorem
MeasureTheory.RCLike.induction
{α : Type u_1}
{𝕂 : Type u_8}
[RCLike 𝕂]
{β : Type u_9}
[Mul β]
{a b : β}
{P : (α → 𝕂) → Prop}
(P_add : ∀ {f g : α → 𝕂}, P f → P g → P (f + g))
(P_components : ∀ {f : α → 𝕂} {c : 𝕂}, c ∈ Components → P f → P (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ component c ∘ f))
(P_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂}, c ∈ Components → P f → P (c • f))
{motive : (α → 𝕂) → β → Prop}
(motive_nnreal :
∀ {f : α → NNReal}, P (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) → motive (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) a)
(motive_add' :
∀ {n : β} {f g : α → 𝕂},
(∀ {x : α}, ‖f x‖ ≤ ‖f x + g x‖) →
(∀ {x : α}, ‖g x‖ ≤ ‖f x + g x‖) → P f → P g → motive f n → motive g n → motive (f + g) (n * b))
(motive_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂} {n : β}, c ∈ Components → P f → motive f n → motive (c • f) n)
⦃f : α → 𝕂⦄
(hf : P f)
:
theorem
MeasureTheory.aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{𝕂 : Type u_8}
[RCLike 𝕂]
{f : α → NNReal}
:
theorem
MeasureTheory.memLorentz_iff_memLorentz_embedRCLike
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{p q : ENNReal}
{𝕂 : Type u_8}
[RCLike 𝕂]
{f : α → NNReal}
:
theorem
MeasureTheory.HasRestrictedWeakType'.of_hasRestrictedWeakType'_nnreal
{α : Type u_1}
{α' : Type u_2}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{p q : ENNReal}
{ε' : Type u_7}
[NoAtoms μ]
{𝕂 : Type u_8}
[RCLike 𝕂]
[TopologicalSpace ε']
[ENormedSpace ε']
{T : (α → 𝕂) → α' → ε'}
(T_meas : ∀ {f : α → 𝕂}, MemLorentz f p 1 μ → AEStronglyMeasurable (T f) ν)
(T_zero : T 0 =ᶠ[ae ν] 0)
(T_subadd :
∀ {f g : α → 𝕂}, MemLorentz f p 1 μ → MemLorentz g p 1 μ → ∀ᵐ (x : α') ∂ν, ‖T (f + g) x‖ₑ ≤ ‖T f x‖ₑ + ‖T g x‖ₑ)
(T_submul : ∀ (a : 𝕂) (f : α → 𝕂), ∀ᵐ (x : α') ∂ν, ‖T (a • f) x‖ₑ ≤ ‖a‖ₑ * ‖T f x‖ₑ)
{c : ENNReal}
(hT_nnreal : HasRestrictedWeakType' (fun (f : α → NNReal) => T (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f)) p q μ ν c)
:
HasRestrictedWeakType' T p q μ ν (4 * c)
theorem
MeasureTheory.HasRestrictedWeakType.hasLorentzType
{α : Type u_1}
{α' : Type u_2}
{m0 : MeasurableSpace α}
{m : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{ε' : Type u_7}
{𝕂 : Type u_8}
[RCLike 𝕂]
[TopologicalSpace ε']
[ENormedSpace ε']
{T : (α → 𝕂) → α' → ε'}
{p q : ENNReal}
(hpq : p.HolderConjugate q)
(p_ne_top : p ≠ ⊤)
(q_ne_top : q ≠ ⊤)
[NoAtoms μ]
[SigmaFinite ν]
{c : NNReal}
(c_pos : 0 < c)
(hT : HasRestrictedWeakType T p q μ ν ↑c)
(T_meas : ∀ {f : α → 𝕂}, MemLorentz f p 1 μ → AEStronglyMeasurable (T f) ν)
(T_subadd :
∀ {f g : α → 𝕂}, MemLorentz f p 1 μ → MemLorentz g p 1 μ → ∀ᵐ (x : α') ∂ν, ‖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 : ℕ → α → 𝕂},
MemLorentz f p 1 μ →
(∀ (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)
(T_zero : T 0 =ᶠ[ae ν] 0)
(T_ae_eq_of_ae_eq : ∀ {f g : α → 𝕂}, f =ᶠ[ae μ] g → T f =ᶠ[ae ν] T g)
:
HasLorentzType T p 1 p ⊤ μ ν (4 * ↑c / p)