fpvandoorn/carleson
Source indexedlemma · leanprover/lean4:v4.32.0
MeasureTheory.weaktype_aux₀
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:921 to 932
Source documentation
If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f
vanishes, then the q-norm of T f vanishes.
Exact Lean statement
lemma weaktype_aux₀ {f : α → ε₁} {T : (α → ε₁) → (α' → ε₂)}
{q₀ p : ℝ≥0∞} (p₀ q : ℝ≥0∞) (hq₀ : 0 < q₀) (hp : 0 < p)
{C₀ : ℝ≥0} (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
(hf : AEStronglyMeasurable f μ) (hF : eLpNorm f p μ = 0) : eLpNorm (T f) q ν = 0Complete declaration
Lean source
Full Lean sourceLean 4
lemma weaktype_aux₀ {f : α → ε₁} {T : (α → ε₁) → (α' → ε₂)} {q₀ p : ℝ≥0∞} (p₀ q : ℝ≥0∞) (hq₀ : 0 < q₀) (hp : 0 < p) {C₀ : ℝ≥0} (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (hf : AEStronglyMeasurable f μ) (hF : eLpNorm f p μ = 0) : eLpNorm (T f) q ν = 0 := by have hf₂ : eLpNorm f p₀ μ = 0 := eLpNorm_eq_zero_of_eLpNorm_eq_zero hf hp.ne' hF have hf₁ : MemLp f p₀ μ := ⟨hf, 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 hq₀.ne').mp wnorm_0 rw [← eLpNorm_enorm] apply eLpNorm_eq_zero_of_ae_zero this