OAI/Probability/GammaPassage/UniformShapeGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.UniformShapeBridge.latticeFloor_mem_box line 9
2. theorem OAI.GammaFPP.UniformShapeBridge.latticeDistance_floor_le line 27
3. theorem OAI.GammaFPP.UniformShapeBridge.uniform_on_unit_ball_of_dense_limits line 48
4. def OAI.GammaFPP.UniformShapeBridge.rescaledPassage line 98
5. theorem OAI.GammaFPP.UniformShapeBridge.rescaledPassage_lattice_error line 101
6. theorem OAI.GammaFPP.UniformShapeBridge.uniform_rescaled_ball_bound line 115

   Source documentation

   Inside-ball version needed in cr:local-travel, at a fixed integer radius multiplier. Arbitrary fixed positive multipliers are bounded by an integer.

   theorem uniform_rescaled_ball_bound (w : Edge → ℝ) (μ : Plane → ℝ)
       (hμ : TimeConstantNorm μ)
       (hu : ∀ ε > 0, ∀ᶠ n : ℕ in atTop, ∀ v, ‖v‖ ≤ 1 →
         |rescaledPassage w n v-μ v| < ε)
       (C : ℕ) (hC : 0 < C) (ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ n : ℕ in atTop, ∀ z : Vertex, ‖latticeEmbed z‖ ≤ (C : ℝ)*n →
         |passageTime w 0 z-μ (latticeEmbed z)| ≤ ε*n := by
   …

   Mentions: OAI.GammaFPP.UniformShapeBridge.rescaledPassage

7. def OAI.GammaFPP.UniformShapeBridge.UniformShape line 148

   Source documentation

   Uniform shape convergence gives the epsilon-radius estimate for all lattice endpoints inside a linearly growing ball.

   def UniformShape (w : Edge → ℝ) (μ : Plane → ℝ) : Prop :=
   …

8. theorem OAI.GammaFPP.UniformShapeBridge.uniformShape_of_uniform_rescaled line 152
9. theorem OAI.GammaFPP.UniformShapeBridge.uniform_inside_ball_real_of_integer line 191

   Source documentation

   Real-scale inside-ball consequence. This is deterministic and law-free; ceil only changes the eventually-large scale by at most a factor two.

   theorem uniform_inside_ball_real_of_integer
       (w : Edge → ℝ) (μ : Plane → ℝ)
       (hu : ∀ C : ℕ, 0 < C → ∀ ε > 0,
         ∀ᶠ n : ℕ in atTop, ∀ z : Vertex, ‖latticeEmbed z‖ ≤ (C : ℝ)*n →
         |passageTime w 0 z-μ (latticeEmbed z)| ≤ ε*n)
       (C : ℝ) (hC : 0 < C) (ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ s : ℝ in atTop, ∀ z : Vertex, ‖latticeEmbed z‖ ≤ C*s →
         |passageTime w 0 z-μ (latticeEmbed z)| ≤ ε*s := by
   …