Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegral_exp_neg_mul_const_mul_self

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1471 to 1486

Source documentation

Exact integral of the derivative of -exp (-a * x) on a finite interval.

Exact Lean statement

theorem intervalIntegral_exp_neg_mul_const_mul_self (a R B : ℝ) :
    ∫ x in R..B, a * Real.exp (-a * x) =
      Real.exp (-a * R) - Real.exp (-a * B)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegral_exp_neg_mul_const_mul_self (a R B : ℝ) :    ∫ x in R..B, a * Real.exp (-a * x) =      Real.exp (-a * R) - Real.exp (-a * B) := by  have hderiv : ∀ x ∈ Set.uIcc R B,      HasDerivAt (fun y : ℝ => -Real.exp (-a * y)) (a * Real.exp (-a * x)) x := by    intro x _hx    have hlin : HasDerivAt (fun y : ℝ => -a * y) (-a) x := by      simpa using (hasDerivAt_id x).const_mul (-a)    have h := (Real.hasDerivAt_exp (-a * x)).comp x hlin    rw [show a * Real.exp (-a * x) = -(Real.exp (-a * x) * -a) from by ring]    exact h.neg  have hint : IntervalIntegrable (fun x : ℝ => a * Real.exp (-a * x)) volume R B := by    apply Continuous.intervalIntegrable    fun_prop  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hderiv hint]  ring