LocalPassageMGF.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_mgf_recursion line 14

Source documentation

Efron–Stein applied to exp (a * F / 2) gives a recursion for the local passage-time moment-generating function.

theorem finitePassageTime_mgf_recursion {shape rate : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) (a : ℝ) (ha : |a| ≤ rate/4) :
    mgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) a ≤
      (mgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) (a/2))^2 +
      ((16*(2 : ℝ)^shape/rate^2)*a^2*R) *
        mgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) a := by
…

Mentions: OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.finiteGammaMeasure

lemma OAI.GammaFPP.FiniteLocal.neg_log_one_sub_le line 79
Source documentation
The negative logarithm of 1 - x is at most 2 * x for 0 ≤ x ≤ 1 / 2.
```
private lemma neg_log_one_sub_le (x : ℝ) (hx : 0 ≤ x) (hx' : x ≤ 1/2) :
    -log (1-x) ≤ 2*x := by
…
```

theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_cgf_recursion line 92

Source documentation

Signed log-MGF recursion; the smallness condition is explicit.

theorem finitePassageTime_cgf_recursion {shape rate : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) (a : ℝ) (ha : |a| ≤ rate/4)
    (hq : (16*(2 : ℝ)^shape/rate^2)*a^2*R ≤ 1/2) :
    cgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) a ≤
      2*cgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) (a/2) +
      2*((16*(2 : ℝ)^shape/rate^2)*a^2*R) := by
…

Mentions: OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.finiteGammaMeasure