OAI/Probability/GammaPassage/ASMeanBridge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.ae_tendsto_zero_of_summable_deviations line 14

   Source documentation

   Summable deviations at the countable tolerances 1 / (k + 1) imply almost-sure convergence to zero. The events need not be measurable.

   theorem ae_tendsto_zero_of_summable_deviations (X : ℕ → Ω → ℝ)
       (hsum : ∀ k : ℕ,
         (∑' n, P {ω | 1 / ((k : ℝ) + 1) ≤ |X n ω|}) ≠ ⊤) :
       ∀ᵐ ω ∂P, Tendsto (fun n => X n ω) atTop (𝓝 0) := by
   …

2. theorem OAI.GammaFPP.ae_tendsto_of_summable_centered_deviations line 30

   Source documentation

   Add a convergent deterministic center after Borel--Cantelli.

   theorem ae_tendsto_of_summable_centered_deviations
       (X : ℕ → Ω → ℝ) (a : ℕ → ℝ) (L : ℝ)
       (ha : Tendsto a atTop (𝓝 L))
       (hsum : ∀ k : ℕ,
         (∑' n, P {ω | 1 / ((k : ℝ) + 1) ≤ |X n ω - a n|}) ≠ ⊤) :
       ∀ᵐ ω ∂P, Tendsto (fun n => X n ω) atTop (𝓝 L) := by
   …

3. theorem OAI.GammaFPP.GammaEnvironment.ae_lattice_limit_of_summable_deviations line 42

   Source documentation

   Summable centered lattice-passage deviations identify the almost-sure limit with the Fekete limit of the means.

   theorem GammaEnvironment.ae_lattice_limit_of_summable_deviations
       {τ : Edge → Ω → ℝ} {shape rate : ℝ}
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (z : Vertex)
       (hsum : ∀ k : ℕ, (∑' n : ℕ, P {ω |
         1 / ((k : ℝ) + 1) ≤
           |passageTime (fun e => τ e ω) 0 (n • z) / (n : ℝ) -
             meanPassageSequence P τ z n / (n : ℝ)|}) ≠ ⊤) :
       ∀ᵐ ω ∂P, Tendsto
         (fun n : ℕ => passageTime (fun e => τ e ω) 0 (n • z) / (n : ℝ))
         atTop (𝓝 (directionalMeanConstant h hs hr z)) :=
   …

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