hasSum_intervalIntegral_comp_add_int

English

If f is integrable, then HasSum of ∫ over shifted unit intervals equals the total integral.

Русский

Если f интегрируема, тогда сумма по интервалам вида [y+n, y+n+1] эквивалентна интегралу по всей области.

LaTeX

$$HasSum (fun n => ∫ x in y+n..y+n+1, f x ∂μ) (∫ x, f x ∂μ).$$

Lean4

theorem _root_.MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int (hfi : Integrable f) :
    HasSum (fun n : ℤ => ∫ x in (0 : ℝ)..(1 : ℝ), f (x + n)) (∫ x, f x) := by
  simpa only [integral_comp_add_right, zero_add, add_comm (1 : ℝ)] using hfi.hasSum_intervalIntegral 0

Похожие утверждения