UniformShape.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.UniformShapeBridge.rescaledPassage_modulus line 14

Source documentation

Deterministic upgrade of a coefficient-A spatial bound.

theorem rescaledPassage_modulus (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (A : ℝ) (hA : 0 < A)
    (hc : ∀ k : ℕ, ∀ᶠ n : ℕ in atTop, ∀ p ∈ latticeBox n, ∀ q ∈ latticeBox n,
      passageTime w p q < A*(latticeDistance p q : ℝ)+(1/(k+1 : ℝ))*n) :
    ∀ ε > 0, ∀ᶠ n in atTop, ∀ v u, ‖v‖ ≤ 2 → ‖u‖ ≤ 2 →
      |rescaledPassage w n v-rescaledPassage w n u| ≤ (2*A)*‖v-u‖+ε := by
…

Mentions: OAI.GammaFPP.UniformShapeBridge.rescaledPassage

theorem OAI.GammaFPP.GammaEnvironment.ae_rescaledPassage_modulus line 54

Source documentation

Countable tolerances only; the endpoint pair may be chosen adaptively on the resulting event. The spatial coefficient is the actual Gamma allowance.

theorem GammaEnvironment.ae_rescaledPassage_modulus
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ ε > 0, ∀ᶠ n in atTop, ∀ v u, ‖v‖ ≤ 2 → ‖u‖ ≤ 2 →
      |rescaledPassage (fun e => τ e ω) n v-rescaledPassage (fun e => τ e ω) n u| ≤
        (2*coordinateAllowance shape rate)*‖v-u‖+ε := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.coordinateAllowance

theorem OAI.GammaFPP.GammaEnvironment.ae_uniform_rescaledPassage line 72

Source documentation

Uniform convergence on the closed Euclidean unit ball for the actual constructed Gamma mean norm. There is no arbitrary norm/shape premise.

theorem GammaEnvironment.ae_uniform_rescaledPassage
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ ε > 0, ∀ᶠ n : ℕ in atTop, ∀ v, ‖v‖ ≤ 1 →
      |rescaledPassage (fun e => τ e ω) n v-gammaMeanNorm h hs hr v| < ε := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.uniform_shape line 94
Source documentation
Exact origin-fixed, same-event all-lattice-endpoint uniform shape. The embedding is the literal Euclidean coordinate embedding extracted in RealDirectionBridge; adaptive endpoints are allowed after the AE quantifier.
```
theorem GammaEnvironment.uniform_shape
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, UniformShapeBridge.UniformShape (fun e => τ e ω) (gammaMeanNorm h hs hr) := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.UniformShapeBridge.UniformShape, OAI.GammaFPP.gammaMeanNorm

theorem OAI.GammaFPP.GammaEnvironment.ae_uniform_inside_ball line 101

Source documentation

Integer-scale inside-ball estimate, with all C and epsilon on one event.

theorem GammaEnvironment.ae_uniform_inside_ball
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ C : ℕ, 0 < C → ∀ ε > 0,
      ∀ᶠ n : ℕ in atTop, ∀ z : Vertex, ‖latticeEmbed z‖ ≤ (C : ℝ)*n →
      |passageTime (fun e => τ e ω) 0 z-gammaMeanNorm h hs hr (latticeEmbed z)| ≤ ε*n := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.ae_uniform_inside_ball_real line 112

Source documentation

Real-scale local-travel form, still origin-fixed and all endpoints on the same AE event. No stationarity or simultaneous moving-origin assertion here.

theorem GammaEnvironment.ae_uniform_inside_ball_real
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ C > 0, ∀ ε > 0,
      ∀ᶠ s : ℝ in atTop, ∀ z : Vertex, ‖latticeEmbed z‖ ≤ C*s →
      |passageTime (fun e => τ e ω) 0 z-gammaMeanNorm h hs hr (latticeEmbed z)| ≤ ε*s := by
…

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