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

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} : HasStrongType T p q μ ν c ↔ HasLorentzType T p p q q μ ν c

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

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.

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 α') : MeasurableSet F → MeasurableSet G → eLpNorm (T (F.indicator fun (x : α) => 1)) 1 (ν.restrict G) ≤ ↑c * μ F ^ p⁻¹.toReal * ν G ^ q⁻¹.toReal

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

An enhanced version of HasRestrictedWeakType

Equations

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

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

The weak continuity assumption needed for HasRestrictedWeakType.hasLorentzType_helper.

Equations

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

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.memLorentz_iff_memLorentz_embedRCLike {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {p q : ENNReal} {𝕂 : Type u_8} [RCLike 𝕂] {f : α → NNReal} : MemLorentz (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) p q μ ↔ MemLorentz f p q μ

theorem MeasureTheory.HasRestrictedWeakType'.of_hasRestrictedWeakType'_nnreal {α : Type u_1} {α' : Type u_2} {m0 : MeasurableSpace α} {m : MeasurableSpace α'} {μ : Measure α} {ν : Measure α'} {p q : ENNReal} {ε' : Type u_7} {𝕂 : 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 ≠ ⊤) [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)