fpvandoorn/carleson
Source indexedlemma · leanprover/lean4:v4.32.0
MeasureTheory.exists_hasStrongType_real_interpolation_aux₀
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:969 to 990
Source documentation
The trivial case for the estimate in the real interpolation theorem
when the L^p norm of f vanishes.
Exact Lean statement
lemma exists_hasStrongType_real_interpolation_aux₀ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
[TopologicalSpace E₁] [ESeminormedAddMonoid E₁] [TopologicalSpace E₂] [ContinuousENorm E₂]
(hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1)
{C₀ : ℝ≥0}
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(h₀T : HasWeakType T p₀ q₀ μ ν C₀)
(h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p) (hf : MemLp f p μ)
(hF : eLpNorm f p μ = 0) :
eLpNorm (T f) q ν = 0Complete declaration
Lean source
Full Lean sourceLean 4
lemma exists_hasStrongType_real_interpolation_aux₀ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] [TopologicalSpace E₂] [ContinuousENorm E₂] (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1) {C₀ : ℝ≥0} (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p) (hf : MemLp f p μ) (hF : eLpNorm f p μ = 0) : eLpNorm (T f) q ν = 0 := by have p_pos : 0 < p := interpolated_pos' hp₀.1 hp₁.1 (ne_top_of_Ioo ht) hp have q₀pos : 0 < q₀ := pos_of_rb_Ioc hp₀ have q₁pos : 0 < q₁ := pos_of_rb_Ioc hp₁ have q_pos : 0 < q := interpolated_pos' q₀pos q₁pos (ne_top_of_Ioo ht) hq have hf₂ : eLpNorm f p₀ μ = 0 := eLpNorm_eq_zero_of_eLpNorm_eq_zero hf.1 p_pos.ne' hF have hf₁ : MemLp f p₀ μ := ⟨hf.1, by rw [hf₂]; exact zero_lt_top⟩ have := (h₀T f hf₁).2 rw [hf₂, mul_zero] at this have wnorm_0 : wnorm (T f) q₀ ν = 0 := nonpos_iff_eq_zero.mp this have : (fun y ↦ ‖(T f) y‖ₑ) =ᵐ[ν] 0 := (wnorm_eq_zero_iff q₀pos.ne').mp wnorm_0 rwa [← eLpNorm_enorm, eLpNorm_eq_zero_iff _ q_pos.ne'] have := h₂T hf; fun_prop