OAI/Probability/GammaPassage/EndpointAsymptotics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.endpoint_mesh_ratio_tendsto line 11

   Source documentation

   The coarse mesh dominates the transverse scale at every fixed level. The integer unit-mesh cutoff requires no separate limiting argument.

   lemma endpoint_mesh_ratio_tendsto {ι : Type*} {l : Filter ι} (k m : ι → ℕ)
       (hratio : Tendsto (fun i => (2 : ℝ)^(m i)/(2 : ℝ)^(k i)) l atTop) (J : ℕ) :
       Tendsto (fun i => (gridMesh (m i) J : ℝ)/(2 : ℝ)^(k i)) l atTop := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.gridMesh

2. lemma OAI.GammaFPP.CrossingBridge.endpoint_levels_eventually line 24
3. lemma OAI.GammaFPP.CrossingBridge.endpoint_error_eventually line 43