Source indexedlemma · leanprover/lean4:v4.32.0

setLIntegral_nnreal_Ici

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:643 to 657

Mathematical statement

Exact Lean statement

lemma setLIntegral_nnreal_Ici {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} :
    ∫⁻ (t : ℝ≥0) in Set.Ici a, f t = ∫⁻ (t : ℝ≥0), f (t + a)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma setLIntegral_nnreal_Ici {f : ℝ≥0 → ℝ≥0∞} {a : ℝ≥0} :    ∫⁻ (t : ℝ≥0) in Set.Ici a, f t = ∫⁻ (t : ℝ≥0), f (t + a) := by  rw [lintegral_nnreal_eq_lintegral_Ici_ofReal, ← lintegral_shift' (a := -a)]  simp only [preimage_add_const_Ici, sub_neg_eq_add, zero_add]  rw [lintegral_nnreal_Ici_eq_lintegral_Ici_ofReal]  apply setLIntegral_congr_fun measurableSet_Ici  intro x hx  simp only  congr  have : (a : ℝ).toNNReal = a := by exact Real.toNNReal_coe  nth_rw 2 [← this]  rw [← Real.toNNReal_add]  · simp only [neg_add_cancel_right]  · simpa  · exact zero_le_coe