Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.HasWeakType.const_smul'

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:741 to 751

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma HasWeakType.const_smul' [IsBoundedSMul 𝕜 E'] {T : (α → ε) → (α' → E')} (hp' : p' ≠ 0)    {c : ℝ≥0∞} (h : HasWeakType T p p' μ ν c) (k : 𝕜) :    HasWeakType (k • T) p p' μ ν (‖k‖ₑ * c) := by  intro f hf  refine ⟨aestronglyMeasurable_const.smul (h f hf).1, ?_⟩  calc wnorm ((k • T) f) p' ν    _ ≤ ‖k‖ₑ * wnorm (T f) p' ν := by simp [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]