OAI/Probability/GammaPassage/MovingOrigin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.IntervalTravelBridge.measureReal_tendsto_zero_of_ae_eventually_notMem line 11
2. def OAI.GammaFPP.IntervalTravelBridge.GoodOrigin line 31
3. theorem OAI.GammaFPP.IntervalTravelBridge.measurableSet_goodOrigin line 38
4. theorem OAI.GammaFPP.IntervalTravelBridge.moving_origin_failure_tendsto line 58

   Source documentation

   Equality in law holds separately at each scale; a may vary arbitrarily.

   theorem moving_origin_failure_tendsto
       (h : IidEnvironment ν P τ) (A : ℕ → Set (Edge → ℝ))
       (hA : ∀ n, MeasurableSet (A n)) (a : ℕ → Vertex)
       (ht : Tendsto (fun n => P.real {ω | (fun e => τ e ω) ∉ A n}) atTop (𝓝 0)) :
       Tendsto (fun n => P.real {ω | (fun e => τ (shiftEdge (a n) e) ω) ∉ A n})
         atTop (𝓝 0) := by
   …

   Mentions: OAI.GammaFPP.IidEnvironment

5. theorem OAI.GammaFPP.IntervalTravelBridge.ae_eventually_gamma_goodOrigin line 71

   Source documentation

   Actual origin good tests, with the norm lower coefficient already derived.

   theorem ae_eventually_gamma_goodOrigin
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (C : ℕ) (hC : 0 < C) (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) :
       ∀ᵐ ω ∂P, ∀ᶠ n : ℕ in atTop,
         GoodOrigin (gammaMeanNorm h hs hr) (cheapSlope shape rate) C η δ n
           (fun e => τ e ω) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.IntervalTravelBridge.GoodOrigin, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.cheapSlope

6. theorem OAI.GammaFPP.IntervalTravelBridge.gamma_moving_goodOrigin_failure_tendsto line 85

   Source documentation

   GoodOrigin failures vanish even for deterministic origins chosen anew at each scale. Endpoint geometry is not part of this probability statement.

   theorem gamma_moving_goodOrigin_failure_tendsto
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (C : ℕ) (hC : 0 < C) (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ)
       (a : ℕ → Vertex) :
       Tendsto (fun n => P.real {ω | ¬GoodOrigin (gammaMeanNorm h hs hr)
         (cheapSlope shape rate) C η δ n (fun e => τ (shiftEdge (a n) e) ω)})
         atTop (𝓝 0) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.IntervalTravelBridge.GoodOrigin, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.cheapSlope