Source indexedlemma · leanprover/lean4:v4.32.0

integral_deriv_mul_add_const

PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:28 to 39

Mathematical statement

Exact Lean statement

lemma integral_deriv_mul_add_const (c : 𝕜) (hab : a ≤ b) (h_int : IntervalIntegrable (deriv f) volume a b)
    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) :
    ∫ t in a..b, (t + c) * deriv f t = (b + c) * f b - (a + c) * f a - ∫ t in a..b, f t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_deriv_mul_add_const (c : 𝕜) (hab : a ≤ b) (h_int : IntervalIntegrable (deriv f) volume a b)    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) :    ∫ t in a..b, (t + c) * deriv f t = (b + c) * f b - (a + c) * f a - ∫ t in a..b, f t := by  rw [← Set.uIcc_of_le hab] at hf_diff  have : ∀ t ∈ [[a, b]], HasDerivAt (fun (t : ℝ) ↦ t + c) 1 t := by    intro t ht    simp only [hasDerivAt_add_const_iff]    convert! ContinuousLinearMap.hasDerivAt (RCLike.ofRealCLM (K := 𝕜)) using 1    simp  replace hf_diff := fun t ht ↦ (hf_diff t ht).hasDerivAt  rw [intervalIntegral.integral_mul_deriv_eq_deriv_mul this hf_diff (by simp) h_int]  simp