Evaluating Integral at Infinity

Stream: new members

[Claus Clausen]

Hey, I am trying to prove the exponential density integrates to 1 but am currently stuck as I can not work around the Infinity in the Interval.
So what I want to show is the following:

import Mathlib.Probability.Notation
import Mathlib.Probability.Density

example {rate : ℝ } (ratePos : 0 < rate) : ↑rate * ∫ (a : ℝ) in Set.Ici 0, Real.exp (-(↑rate * a)) = 1 := sorry

--I thought I might be able to show it by proving that the Intervals [0,n] tend to Set.Ici 0 but I am not sure how to use this information correctly.

example: Filter.Tendsto (fun n : ℕ  => ∫ (a : ℝ) in (Set.Icc (0 : ℝ) ↑n), Real.exp (-(↑rate * a))) Filter.atTop (nhds (∫ a in ⋃ (n : ℕ), (Set.Icc (0 : ℝ) ↑n), Real.exp (-(↑rate * a)))) := sorry

any help how to use the additional information or another direction would be helpful

[Patrick Massot]

You should take a look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.html.