Weak, strong and Lorentz type of operators

The predicates HasWeakType, HasBoundedWeakType, HasStrongType, HasBoundedStrongType and HasLorentzType for operators between function spaces, and their basic properties.

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) : Prop

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.

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) : Prop

A weaker version of HasWeakType.

Equations

• One or more equations did not get rendered due to their size.

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) : Prop

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.

def MeasureTheory.HasLorentzType {α : Type u_1} {α' : Type u_2} {ε₁ : Type u_4} {ε₂ : Type u_5} {m : MeasurableSpace α} {m✝ : MeasurableSpace α'} [ENorm ε₁] [ENorm ε₂] [TopologicalSpace ε₁] [TopologicalSpace ε₂] (T : (α → ε₁) → α' → ε₂) (p r q s : ENNReal) (μ : Measure α) (ν : Measure α') (c : ENNReal) : Prop

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.

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.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 ≠ ⊤) : HasWeakType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c ↔ HasWeakType T p p' μ ν c

theorem MeasureTheory.hasWeakType_iSup_of_monotone {α : Type u_1} {α' : Type u_2} {ε₁ : Type u_4} {m : MeasurableSpace α} {m✝ : MeasurableSpace α'} {p p' c : ENNReal} {μ : Measure α} {ν : Measure α'} [TopologicalSpace ε₁] [ContinuousENorm ε₁] {f : ℕ → (α → ε₁) → α' → ENNReal} (hf : Monotone f) (hp' : p' ≠ 0) (hwtf : ∀ (n : ℕ), HasWeakType (f n) p p' μ ν c) : HasWeakType (fun (u : α → ε₁) (x : α') => ⨆ (n : ℕ), f n u x) p p' μ ν c

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 ε₁] [ESeminormedAddMonoid ε₁] [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 ε₁] [ESeminormedAddMonoid ε₁] [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

theorem MeasureTheory.hasStrongType_iSup_of_monotone {α : Type u_1} {α' : Type u_2} {ε₁ : Type u_4} {m : MeasurableSpace α} {m✝ : MeasurableSpace α'} {p p' c : ENNReal} {μ : Measure α} {ν : Measure α'} [TopologicalSpace ε₁] [ContinuousENorm ε₁] {f : ℕ → (α → ε₁) → α' → ENNReal} (hf : Monotone f) (hstf : ∀ (n : ℕ), HasStrongType (f n) p p' μ ν c) : HasStrongType (fun (u : α → ε₁) (x : α') => ⨆ (n : ℕ), f n u x) 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 ε₁] [ESeminormedAddMonoid ε₁] [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 ε₁] [ESeminormedAddMonoid ε₁] [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 ε₁] [ESeminormedAddMonoid ε₁] [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 ε₁] [ESeminormedAddMonoid ε₁] {T : (α → ε₁) → α' → ENNReal} (h : HasBoundedStrongType T p p' μ ν c) (r : NNReal) : HasBoundedStrongType (r • T) p p' μ ν (r • c)

Comparison with HasLorentzType

theorem MeasureTheory.hasStrongType_iff_hasLorentzType {α : Type u_1} {α' : Type u_2} {ε₁ : Type u_4} {ε₂ : Type u_5} {m : MeasurableSpace α} {m✝ : MeasurableSpace α'} {p q : ENNReal} {μ : Measure α} {ν : Measure α'} [TopologicalSpace ε₁] [TopologicalSpace ε₂] [ESeminormedAddMonoid ε₁] [ESeminormedAddMonoid ε₂] {T : (α → ε₁) → α' → ε₂} {c : ENNReal} : HasStrongType T p q μ ν c ↔ HasLorentzType T p p q q μ ν c

theorem MeasureTheory.hasWeakType_iff_hasLorentzType {α : Type u_1} {α' : Type u_2} {ε₁ : Type u_4} {ε₂ : Type u_5} {m : MeasurableSpace α} {m✝ : MeasurableSpace α'} {p q : ENNReal} {μ : Measure α} {ν : Measure α'} [TopologicalSpace ε₁] [TopologicalSpace ε₂] [ESeminormedAddMonoid ε₁] [ESeminormedAddMonoid ε₂] {T : (α → ε₁) → α' → ε₂} {c : ENNReal} : HasWeakType T p q μ ν c ↔ HasLorentzType T p p q ⊤ μ ν c

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 ε'] [ESeminormedAddCommMonoid ε'] [SMul NNReal ε'] [ENormSMulClass NNReal ε'] [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.HasWeakType.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} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [Module NNReal ε'] [ENormSMulClass NNReal ε'] [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)