Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLpNormEssSup_nnreal_scale_constant'

Carleson.ToMathlib.MeasureTheory.Function.LpNorm.Misc · Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean:34 to 44

Mathematical statement

Exact Lean statement

lemma eLpNormEssSup_nnreal_scale_constant' {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} (h : a ≠ 0)
  (hf : AEStronglyMeasurable f) :
    eLpNormEssSup (fun x ↦ f (a * x)) volume = eLpNormEssSup f volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNormEssSup_nnreal_scale_constant' {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} (h : a ≠ 0)  (hf : AEStronglyMeasurable f) :    eLpNormEssSup (fun x ↦ f (a * x)) volume = eLpNormEssSup f volume := by  calc _    _ = eLpNormEssSup (f ∘ fun x ↦ a * x) volume := by congr  rw [← eLpNormEssSup_map_measure _ (by fun_prop)]  · apply eLpNormEssSup_congr_measure    rw [NNReal.map_volume_mul_left h]    apply Measure.ae_ennreal_smul_measure_eq (by simpa)  · rw [NNReal.map_volume_mul_left h]    apply AEStronglyMeasurable.smul_measure hf