Source indexedlemma · leanprover/lean4:v4.32.0

lintegral_nnreal_scale_constant'

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:659 to 671

Mathematical statement

Exact Lean statement

lemma lintegral_nnreal_scale_constant' {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} (h : a ≠ 0) :
    a * ∫⁻ x : ℝ≥0, f (a*x) = ∫⁻ x, f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lintegral_nnreal_scale_constant' {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} (h : a ≠ 0) :    a * ∫⁻ x : ℝ≥0, f (a*x) = ∫⁻ x, f x := by  rw [lintegral_nnreal_eq_lintegral_toNNReal_Ioi, lintegral_nnreal_eq_lintegral_toNNReal_Ioi]  symm  rw [← lintegral_scale_constant_halfspace' (a:=a) (by rw [NNReal.coe_pos, pos_iff_ne_zero]; exact h)]  congr 1  · simp  apply setLIntegral_congr_fun measurableSet_Ioi  intro x hx  dsimp only  congr  rw [Real.toNNReal_mul (by simp)]  simp