OAI/Probability/GammaPassage/BallTravel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_badConnections_tendsto_zero line 12
2. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_ball_travel_nat line 19
3. theorem OAI.GammaFPP.IntervalTravelBridge.segmentTube_translate_iff line 90
4. theorem OAI.GammaFPP.IntervalTravelBridge.localTravel_translate_iff line 99
5. theorem OAI.GammaFPP.IntervalTravelBridge.measurableSet_ballTravel line 118
6. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_ball_travel line 125
7. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_set_travel line 159

   Source documentation

   Simultaneous travel for arbitrary deterministic lattice endpoint sets of bounded combined diameter. This stronger statement includes vertical intervals.

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

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

8. def OAI.GammaFPP.IntervalTravelBridge.verticalInterval line 183
9. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_interval_travel line 188

   Source documentation

   Travel between vertical intervals of bounded combined Euclidean diameter, including empty and singleton intervals (Lemma cr:interval-travel).

   theorem gamma_interval_travel (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (D η δ : ℝ) (hD : 0 < D) (hη : 0 < η) (hδ : 0 < δ) :
       ∀ ε > 0, ∀ᶠ s : ℝ in atTop, ∀ x₁ x₂ : ℤ, ∀ l₁ u₁ l₂ u₂ : ℝ,
         (∀ p ∈ verticalInterval x₁ l₁ u₁ ∪ verticalInterval x₂ l₂ u₂,
           ∀ q ∈ verticalInterval x₁ l₁ u₁ ∪ verticalInterval x₂ l₂ u₂,
             ‖latticeEmbed (q-p)‖ ≤ D*s) →
         P.real {ω | ¬∀ p ∈ verticalInterval x₁ l₁ u₁, ∀ q ∈ verticalInterval x₂ l₂ u₂,
           LocalTravel (gammaMeanNorm h hs hr) η δ s p q (fun e => τ e ω)} < ε := by
   …

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