OAI/Probability/GammaPassage/TubeTravel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_tube_failure_bound line 11
2. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_tube_travel_nat line 42

   Source documentation

   Uniform probability statement for all deterministic endpoint pairs at each large integer scale. It is NOT one event of simultaneous success for all pairs.

   theorem gamma_tube_travel_nat
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (D η δ : ℝ) (hD : 0 < D) (hη : 0 < η) (hδ : 0 < δ) :
       ∀ ε > 0, ∀ᶠ n : ℕ in atTop, ∀ p q : Vertex,
         ‖latticeEmbed (q-p)‖ ≤ D*n →
         P.real {ω | ¬LocalTravel (gammaMeanNorm h hs hr) η δ n p q (fun e => τ e ω)} < ε := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.IntervalTravelBridge.LocalTravel, OAI.GammaFPP.gammaMeanNorm