PL1/ExponentialTail.lean

All source files · Download exact source

SHA-256: 4269eed74878fd20966a92272cbe96e6f58fb4191bf757d54ed5acc156d4c578

1import PL1.ExponentialTime23/-! # Exact tails of the exponential Laplace transform -/45noncomputable section6open MeasureTheory ProbabilityTheory Set7open scoped NNReal ENNReal89namespace PL1.ExponentialTime1011theorem integral_laplace_Ici {t : ℝ} (ht : 0 < t) (a : ℝ) (ha : 0 ≤ a)12    (ε : ℝ≥0) :13    (∫ u : ℝ≥0 in Ici ε, Real.exp (-(u : ℝ) * a) ∂timeMeasure t) =14      Real.exp (-(ε : ℝ) * (t⁻¹ + a)) * (1 + t * a)⁻¹ := by15  rw [← integral_indicator measurableSet_Ici, timeMeasure,16    integral_map_of_stronglyMeasurable measurable_real_toNNReal17      ((show StronglyMeasurable (fun u : ℝ≥0 => Real.exp (-(u : ℝ) * a)) from18        (by fun_prop)).indicator measurableSet_Ici),19    integral_expMeasure_eq_density (inv_pos.2 ht)]20  have hfun : (fun x : ℝ => exponentialPDFReal t⁻¹ x *21      ((Ici ε).indicator (fun u : ℝ≥0 => Real.exp (-(u : ℝ) * a))) (Real.toNNReal x)) =22      (Ici (ε : ℝ)).indicator (fun x => t⁻¹ * Real.exp (-(t⁻¹ + a) * x)) := by23    funext x24    rw [expDensity_eq]25    by_cases hx : 0 ≤ x26    · have he : ε ≤ Real.toNNReal x ↔ (ε : ℝ) ≤ x := by27        rw [← NNReal.coe_le_coe, Real.coe_toNNReal x hx]28      by_cases hε : (ε : ℝ) ≤ x29      · simp only [Set.indicator, mem_Ici, ite_eq_left hx, ite_eq_left (he.mpr hε),30          ite_eq_left hε, Real.coe_toNNReal x hx]31        rw [mul_assoc, ← Real.exp_add]32        congr 233        ring34      · simp only [Set.indicator, mem_Ici, ite_eq_left hx,35          ite_eq_right (show ¬ ε ≤ Real.toNNReal x from fun h => hε (he.mp h)),36          ite_eq_right hε, mul_zero]37    · rw [ite_eq_right hx, zero_mul, Set.indicator_of_notMem]38      exact fun h => hx (ε.coe_nonneg.trans h)39  rw [hfun, integral_indicator measurableSet_Ici, integral_Ici_eq_integral_Ioi,40    integral_const_mul,41    integral_exp_mul_Ioi (by linarith [inv_pos.2 ht] : -(t⁻¹ + a) < 0) (ε : ℝ)]42  have hden : 1 + t * a ≠ 0 := ne_of_gt (by positivity)43  have hden' : t⁻¹ + a ≠ 0 := ne_of_gt (by positivity)44  rw [show -(t⁻¹ + a) * (ε : ℝ) = -(ε : ℝ) * (t⁻¹ + a) by ring]45  field_simp [ne_of_gt ht, hden, hden']4647theorem integral_laplace_Ici_ofReal {𝕜 : Type*} [RCLike 𝕜] {t : ℝ}48    (ht : 0 < t) (a : ℝ) (ha : 0 ≤ a) (ε : ℝ≥0) :49    (∫ u : ℝ≥0 in Ici ε, (Real.exp (-(u : ℝ) * a) : 𝕜) ∂timeMeasure t) =50      ((Real.exp (-(ε : ℝ) * (t⁻¹ + a)) * (1 + t * a)⁻¹ : ℝ) : 𝕜) := by51  rw [integral_ofReal, integral_laplace_Ici ht a ha]5253end PL1.ExponentialTime54