Source indexedtheorem · leanprover/lean4:v4.32.0

sum_eq_integral_add_integral_deriv

PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:67 to 79

Mathematical statement

Exact Lean statement

theorem sum_eq_integral_add_integral_deriv (ha : 0 ≤ a) (hab : a ≤ b)
    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)
    (h_cont : ContinuousOn (deriv f) [[a, b]]) :
    ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f k =
      f a * B1 a - f b * B1 b + (∫ t in a..b, f t) + ∫ t in a..b, deriv f t * B1 t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sum_eq_integral_add_integral_deriv (ha : 0 ≤ a) (hab : a ≤ b)    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)    (h_cont : ContinuousOn (deriv f) [[a, b]]) :    ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f k =      f a * B1 a - f b * B1 b + (∫ t in a..b, f t) + ∫ t in a..b, deriv f t * B1 t  := by  have := sum_mul_eq_sub_sub_integral_mul (fun _ ↦ 1) ha hab hf_diff (Set.uIcc_of_le hab ▸ h_cont).integrableOn_Icc  simp only [mul_one, sum_const, Nat.card_Icc, tsub_zero, nsmul_eq_mul, Nat.cast_add,    Nat.cast_one] at this  rw [this, ← intervalIntegral.integral_of_le hab]  rw [integral_deriv_mul_floor_add_one ha hab hf_diff h_cont]  unfold B1  push_cast  ring