SpatialModulus.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.gammaBadConnections line 16
Source documentation
Failure of the Gamma allowance for some actual coordinate path in the box.
```
def gammaBadConnections (shape rate : ℝ) (τ : Edge → Ω → ℝ)
    (ε : ℝ) (n : ℕ) : Set Ω :=
…
```

theorem OAI.GammaFPP.GammaEnvironment.gammaBadConnections_probability line 23

Source documentation

Finite union bound over all ordered pairs, without independence of path events.

theorem GammaEnvironment.gammaBadConnections_probability
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (ε : ℝ) (n : ℕ) :
    P.real (gammaBadConnections shape rate τ ε n) ≤
      (2 * (n : ℝ) + 1) ^ 4 * (2 * Real.exp (-(rate / 4) * (ε * n))) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaBadConnections

theorem OAI.GammaFPP.summable_gamma_box_connection_bound line 37

Source documentation

The only summability requirement is positive rate times positive epsilon.

theorem summable_gamma_box_connection_bound {rate ε : ℝ}
    (hr : 0 < rate) (hε : 0 < ε) :
    Summable (fun n : ℕ =>
      (2 * (n : ℝ) + 1) ^ 4 * (2 * Real.exp (-(rate / 4) * (ε * n)))) := by
…

theorem OAI.GammaFPP.GammaEnvironment.ae_eventually_coordinate_connections line 48

Source documentation

For each fixed positive epsilon, almost surely all sufficiently large boxes have the connection estimate for every pair, even pairs selected from the environment.

theorem GammaEnvironment.ae_eventually_coordinate_connections
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    {ε : ℝ} (hε : 0 < ε) :
    ∀ᵐ ω ∂P, ∀ᶠ n : ℕ in atTop, ∀ p ∈ latticeBox n, ∀ q ∈ latticeBox n,
      pathCost (fun e => τ e ω) p (coordinatePath p q) <
        coordinateAllowance shape rate * (latticeDistance p q : ℝ) + ε * n := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.ae_eventually_passageTime_connections line 70

Source documentation

The same modulus for the actual infimum passage time. Fixed epsilon precedes AE; simultaneous control concerns finite-box pairs, not an uncountable family of epsilons.

theorem GammaEnvironment.ae_eventually_passageTime_connections
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    {ε : ℝ} (hε : 0 < ε) :
    ∀ᵐ ω ∂P, ∀ᶠ n : ℕ in atTop, ∀ p ∈ latticeBox n, ∀ q ∈ latticeBox n,
      passageTime (fun e => τ e ω) p q <
        coordinateAllowance shape rate * (latticeDistance p q : ℝ) + ε * n := by
…

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