English
The exponential pdf is positive for all positive rates and positive arguments: 0 < exponentialPDFReal(r, x) when r>0 and x>0.
Русский
Плотность экспоненциального распределения положительна при r>0 и x>0.
LaTeX
$$$ (r>0) \land (x>0) \Rightarrow 0 < \text{exponentialPDFReal}(r, x) $$$
Lean4
theorem 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) :=
by
split_ifs with h
case neg =>
simp only [exponentialPDF_eq]
rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
exact fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
case
pos =>
rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0), zero_add]
simp only [exponentialPDF_eq]
rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
(by intro a ha; simp [ha.1])]
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 _)))]
· have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
· rw [ENNReal.toReal_ofReal_eq_iff.2 (by simp; positivity)]
norm_num; ring
· simp only [intervalIntegrable_iff, uIoc_of_le h]
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
· have : Continuous (fun a ↦ rexp (-(r * a))) := by simp only [← neg_mul]; exact (continuous_mul_left (-r)).rexp
exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this)
· simp only [neg_mul, one_mul]
exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
· refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
exact exp_neg_integrableOn_Ioc hr
· refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
rw [integrableOn_Icc_iff_integrableOn_Ioc]
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
