Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.HasWeakType.const_smul

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:727 to 737

Mathematical statement

Exact Lean statement

lemma HasWeakType.const_smul [ContinuousConstSMul ℝ≥0 ε']
    {T : (α → ε) → (α' → ε')} (hp' : p' ≠ 0) {c : ℝ≥0∞} (h : HasWeakType T p p' μ ν c) (k : ℝ≥0) :
    HasWeakType (k • T) p p' μ ν (k * c)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma HasWeakType.const_smul [ContinuousConstSMul ℝ≥0 ε']    {T : (α → ε) → (α' → ε')} (hp' : p' ≠ 0) {c : ℝ≥0∞} (h : HasWeakType T p p' μ ν c) (k : ℝ≥0) :    HasWeakType (k • T) p p' μ ν (k * c) := by  intro f hf  refine ⟨(h f hf).1.const_smul k, ?_⟩  calc wnorm ((k • T) f) p' ν    _ ≤ k * wnorm (T f) p' ν := by simpa using wnorm_const_smul_le hp' _    _ ≤ k * (c * eLpNorm f p μ) := by      gcongr      apply (h f hf).2    _ = (k * c) * eLpNorm f p μ := by rw [mul_assoc]