-- Mathlib/Probability/Distributions/Exponential.lean
lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
    ∫⁻ y in Iic x, exponentialPDF r y
    = ENNReal.ofReal (if 0 ≤ x then 1 - exp (-(r * x)) else 0)

Proof state:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Tactic:
case neg =>
  simp only [exponentialPDF_eq]
  rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
  exact ae_of_all _ fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

Result:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ Integrable (fun x => rexp (-(r * x))) (ℙ.restrict (Icc 0 x))

Tactic:
rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => rexp (-(r * x))) (Ioc 0 x) ℙ

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))

Tactic:
norm_num

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0

Tactic:
rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun a => -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ Continuous fun a => rexp (-(r * a))

Tactic:
simp only [← neg_mul]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ Continuous fun a => rexp (-r * a)

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ IntervalIntegrable (fun a => r * rexp (-(r * a))) ℙ 0 x

Tactic:
simp only [intervalIntegrable_iff, uIoc_of_le h]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ IntegrableOn (fun a => r * rexp (-(r * a))) (Ioc 0 x) ℙ

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => rexp (-(r * x))) (Ioc 0 x) ℙ

Tactic:
exact exp_neg_integrableOn_Ioc hr

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
  zero_add]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Tactic:
simp only [exponentialPDF_eq]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => r * rexp (-(r * x))) (Ioc 0 x) ℙ

Tactic:
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))

Tactic:
ring

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∀ a ∈ Icc 0 x, ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = ?m.16773 a

Tactic:
intro a ⟨(hle : _ ≤ a), _⟩

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
hle : 0 ≤ a
right✝ : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = ?m.16773 a

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => r * rexp (-(r * x))) (Icc 0 x) ℙ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => r * rexp (-(r * x))) (Ioc 0 x) ℙ

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ¬0 ≤ a

Tactic:
linarith

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ Continuous fun a => rexp (-r * a)

Tactic:
exact (continuous_mul_left (-r)).rexp

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (fun x => r * rexp (-(r * x))) (ℙ.restrict (Icc 0 x))

Tactic:
refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ Integrable (fun x => rexp (-(r * x))) (ℙ.restrict (Icc 0 x))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
simp only [exponentialPDF_eq]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ ContinuousOn (fun a => -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
have : Continuous (fun a ↦ rexp (-(r * a))) := by
  simp only [← neg_mul]; exact (continuous_mul_left (-r)).rexp

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this✝ : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
this : Continuous fun a => rexp (-(r * a))
⊢ ContinuousOn (fun a => -1 * rexp (-(r * a))) (Icc 0 x)

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this✝ : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
this : Continuous fun a => rexp (-(r * a))
⊢ ContinuousOn (fun a => -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this)

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ 0 ≤ 1 - rexp (-(r * x))

Tactic:
norm_num

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ 0 ≤ r * x

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ≠ ⊤

Tactic:
refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x => r * rexp (-(r * x))) (Icc 0 x) ℙ

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [← ENNReal.toReal_eq_toReal _ ENNReal.ofReal_ne_top, ← integral_eq_lintegral_of_nonneg_ae
    (Eventually.of_forall fun _ ↦ le_of_lt (mul_pos hr (exp_pos _)))]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (fun x => r * rexp (-(r * x))) (ℙ.restrict (Icc 0 x))

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ≠ ⊤