OAI/Probability/GammaPassage/RealDirectionBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.RealDirectionBridge.real_scale_connections line 11
2. theorem OAI.GammaFPP.RealDirectionBridge.real_scale_connections_normalized line 48
3. theorem OAI.GammaFPP.RealDirectionBridge.real_direction_limits_of_lattice_limits line 69
4. theorem OAI.GammaFPP.GammaEnvironment.isTimeConstant_of_ae_lattice_limits line 143

   Source documentation

   Almost-sure lattice-ray limits and the Gamma spatial modulus extend the constructed mean norm to a time constant in every fixed real direction.

   theorem GammaEnvironment.isTimeConstant_of_ae_lattice_limits
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {τ : Edge → Ω → ℝ}
       {shape rate : ℝ} (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (hray : ∀ z : Vertex, ∀ᵐ ω ∂P,
         Tendsto (fun n : ℕ => passageTime (fun e => τ e ω) 0 (n • z) / n)
           atTop (𝓝 (directionalMeanConstant h hs hr z))) :
       IsTimeConstant P τ (gammaMeanNorm h hs hr) := by
   …

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