PL1/ExponentialTime.lean
All source files · Download exact source
SHA-256: d01b8ecef17c19cc657a2a7dfce8386be43bf1f82dcf5316a8e9717a61e999aa
1import Mathlib.Probability.Distributions.Exponential2import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals3import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap4import Mathlib.Tactic.FieldSimp5import Mathlib.Tactic.Linarith6import Mathlib.Tactic.Ring78/-!9# The exponential time distribution in the resolvent formula1011`timeMeasure t` is the actual rate-`t⁻¹` exponential distribution transported to12the nonnegative reals. For positive `t` it is a probability measure, and its13Laplace transform is `(1 + t * a)⁻¹` for every `a ≥ 0`.14-/1516noncomputable section17open MeasureTheory ProbabilityTheory Set Filter18open scoped NNReal ENNReal Topology1920namespace PL1.ExponentialTime2122/-- Exponential time with mean `t`, represented on the nonnegative reals. -/23def timeMeasure (t : ℝ) : Measure ℝ≥0 := (expMeasure t⁻¹).map Real.toNNReal2425theorem isProbabilityMeasure_timeMeasure {t : ℝ} (ht : 0 < t) :26 IsProbabilityMeasure (timeMeasure t) := by27 let : IsProbabilityMeasure (expMeasure t⁻¹) :=28 isProbabilityMeasure_expMeasure (inv_pos.2 ht)29 unfold timeMeasure30 infer_instance3132theorem expDensity_eq (r x : ℝ) :33 exponentialPDFReal r x = if 0 ≤ x then r * Real.exp (-(r * x)) else 0 := by34 simp [exponentialPDFReal, gammaPDFReal]3536/-- Integrating against the standard exponential distribution uses its genuine density. -/37theorem integral_expMeasure_eq_density {r : ℝ} (hr : 0 < r) (f : ℝ → ℝ) :38 (∫ x, f x ∂expMeasure r) = ∫ x, exponentialPDFReal r x * f x := by39 change (∫ x, f x ∂volume.withDensity (fun x => ENNReal.ofReal (exponentialPDFReal r x))) = _40 rw [integral_withDensity_eq_integral_toReal_smul41 ((measurable_exponentialPDFReal r).ennreal_ofReal)42 (ae_of_all _ (fun x => ENNReal.ofReal_lt_top))]43 simp only [ENNReal.toReal_ofReal (exponentialPDFReal_nonneg hr _), smul_eq_mul]4445theorem exp_neg_mul_norm_le_one (a : ℝ) (ha : 0 ≤ a) (u : ℝ≥0) :46 ‖Real.exp (-(u : ℝ) * a)‖ ≤ 1 := by47 rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]48 apply Real.exp_le_one_iff.249 exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.2 u.coe_nonneg) ha5051theorem integrable_laplace {t : ℝ} (ht : 0 < t) (a : ℝ) (ha : 0 ≤ a) :52 Integrable (fun u : ℝ≥0 => Real.exp (-(u : ℝ) * a)) (timeMeasure t) := by53 let := isProbabilityMeasure_timeMeasure ht54 apply Integrable.of_bound (by fun_prop) 155 exact ae_of_all _ (exp_neg_mul_norm_le_one a ha)5657/-- The Laplace transform of the actual exponential time law. -/58theorem integral_laplace {t : ℝ} (ht : 0 < t) (a : ℝ) (ha : 0 ≤ a) :59 (∫ u : ℝ≥0, Real.exp (-(u : ℝ) * a) ∂timeMeasure t) = (1 + t * a)⁻¹ := by60 rw [timeMeasure, integral_map_of_stronglyMeasurable measurable_real_toNNReal (by fun_prop),61 integral_expMeasure_eq_density (inv_pos.2 ht)]62 have hfun : (fun x : ℝ => exponentialPDFReal t⁻¹ x * Real.exp (-(Real.toNNReal x : ℝ) * a)) =63 (Ici (0 : ℝ)).indicator (fun x => t⁻¹ * Real.exp (-(t⁻¹ + a) * x)) := by64 funext x65 rw [expDensity_eq]66 by_cases hx : 0 ≤ x67 · simp only [Set.indicator, mem_Ici, ite_eq_left hx, Real.coe_toNNReal x hx]68 rw [mul_assoc, ← Real.exp_add]69 congr 270 ring71 · simp only [Set.indicator, mem_Ici, ite_eq_right hx, zero_mul]72 rw [hfun, integral_indicator measurableSet_Ici, integral_Ici_eq_integral_Ioi, integral_const_mul,73 integral_exp_mul_Ioi (by linarith [inv_pos.2 ht] : -(t⁻¹ + a) < 0) 0]74 simp only [mul_zero, Real.exp_zero, neg_div]75 have hden : 1 + t * a ≠ 0 := ne_of_gt (by positivity)76 have hden' : t⁻¹ + a ≠ 0 := ne_of_gt (by positivity)77 field_simp [ne_of_gt ht, hden, hden']7879theorem integral_laplace_ofReal {𝕜 : Type*} [RCLike 𝕜] {t : ℝ}80 (ht : 0 < t) (a : ℝ) (ha : 0 ≤ a) :81 (∫ u : ℝ≥0, (Real.exp (-(u : ℝ) * a) : 𝕜) ∂timeMeasure t) =82 ((1 + t * a)⁻¹ : ℝ) := by83 rw [integral_ofReal, integral_laplace ht a ha]8485end PL1.ExponentialTime86