OAI/Probability/GammaPassage/SequenceSummability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.exp_neg_sqrt_le line 11
2. lemma OAI.GammaFPP.summable_exp_neg_sqrt line 23
3. def OAI.GammaFPP.localizationDecay line 32
4. lemma OAI.GammaFPP.localizationDecay_pos line 35
5. lemma OAI.GammaFPP.localizationErrorBound_exp line 39
6. lemma OAI.GammaFPP.exists_ray_cutoff line 63

   Source documentation

   Choose a natural length multiplier; it may depend on direction and law, never on sample, time n, or deviation threshold.

   lemma exists_ray_cutoff {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate) (d : ℕ) :
       ∃ L : ℕ, d < L ∧ 2*coordinateAllowance shape rate*(d : ℝ) ≤ cheapSlope shape rate*L := by
   …

   Mentions: OAI.GammaFPP.coordinateAllowance, OAI.GammaFPP.cheapSlope

7. lemma OAI.GammaFPP.meanLocalizationAllowance_mul line 73
8. theorem OAI.GammaFPP.GammaEnvironment.summable_ray_centered_deviations line 87

   Source documentation

   Absolute centered deviations at every positive lattice-ray index are summable. Zero direction needs no special denominator or positive distance.

   theorem GammaEnvironment.summable_ray_centered_deviations
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (z : Vertex) (ε : ℝ) (hε : 0 < ε) :
       Summable (fun n : ℕ => P.real {ω | ε*(n+1 : ℝ) ≤
         |passageTime (fun e => τ e ω) 0 ((n+1) • z) -
           meanPassageSequence P τ z (n+1)|}) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence

9. theorem OAI.GammaFPP.GammaEnvironment.normalized_ray_deviations_tsum_ne_top line 181

   Source documentation

   Normalized centered deviations along a lattice ray have summable probabilities at every positive tolerance. The event at n = 0 is empty.

   theorem GammaEnvironment.normalized_ray_deviations_tsum_ne_top
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (z : Vertex) (k : ℕ) :
       (∑' n : ℕ, P {ω | 1/((k : ℝ)+1) ≤
         |passageTime (fun e => τ e ω) 0 (n • z)/(n : ℝ) -
           meanPassageSequence P τ z n/(n : ℝ)|}) ≠ ⊤ := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence