ExponentialIncrement.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.abs_exp_sub_one_le_abs_mul_exp_abs line 13
Source documentation
Global, signed version of the elementary exponential increment estimate.
```
lemma abs_exp_sub_one_le_abs_mul_exp_abs (x : ℝ) :
    |exp x - 1| ≤ |x| * exp |x| := by
…
```

lemma OAI.GammaFPP.half_exp_increment_square_domination line 29

Source documentation

Pointwise domination on the support; it also covers u=0 and a=0.

lemma half_exp_increment_square_domination {rate a u : ℝ}
    (hrate : 0 < rate) (ha : |a| ≤ rate / 4) (hu : 0 ≤ u) :
    (exp (a*u/2)-1)^2 ≤ (8 / rate^2 * a^2) * exp ((rate/2)*u) := by
…

theorem OAI.GammaFPP.gamma_integrable_half_exp_increment_square line 72

Source documentation

Integrability follows from a positive Gamma moment at rate/2.

theorem gamma_integrable_half_exp_increment_square {shape rate a : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (ha : |a| ≤ rate/4) :
    Integrable (fun u : ℝ => (exp (a*u/2)-1)^2) (gammaMeasure shape rate) := by
…

theorem OAI.GammaFPP.gamma_integral_half_exp_increment_square_le line 83

Source documentation

Signed quadratic increment estimate for all positive shape and rate.

theorem gamma_integral_half_exp_increment_square_le {shape rate a : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (ha : |a| ≤ rate/4) :
    (∫ u : ℝ, (exp (a*u/2)-1)^2 ∂gammaMeasure shape rate) ≤
      (8*(2 : ℝ)^shape/rate^2)*a^2 := by
…