CheapLongTrails.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.cheapTrailEvent line 15
Source documentation
Cheap trails at one exact length and one deterministic starting vertex.
```
def cheapTrailEvent (shape rate : ℝ) (τ : Edge → Ω → ℝ)
    (p : Vertex) (n : ℕ) : Set Ω :=
…
```
theorem OAI.GammaFPP.GammaEnvironment.summable_cheapTrailEvent_real line 22
Source documentation
Exponential decay is summable, including the nonempty bad event at n=0.
```
theorem GammaEnvironment.summable_cheapTrailEvent_real
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (p : Vertex) : Summable (fun n => P.real (cheapTrailEvent shape rate τ p n)) := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.cheapTrailEvent

theorem OAI.GammaFPP.GammaEnvironment.ae_long_trails_cost line 32

Source documentation

At each fixed start, almost surely all sufficiently long trails have strictly positive linear cost. No independence across lengths is used.

theorem GammaEnvironment.ae_long_trails_cost
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (p : Vertex) :
    ∀ᵐ ω ∂P, ∃ N : ℕ, ∀ ds : List Step, N ≤ ds.length →
      ((trace p ds).map traversalEdge).Nodup →
        cheapSlope shape rate * (ds.length : ℝ) < pathCost (fun e => τ e ω) p ds := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.cheapSlope

theorem OAI.GammaFPP.GammaEnvironment.ae_all_starts_long_trails_cost line 51

Source documentation

Countably many lattice starts may share one event; the length cutoff can depend on both the environment and the start.

theorem GammaEnvironment.ae_all_starts_long_trails_cost
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ p : Vertex, ∃ N : ℕ, ∀ ds : List Step, N ≤ ds.length →
      ((trace p ds).map traversalEdge).Nodup →
        cheapSlope shape rate * (ds.length : ℝ) < pathCost (fun e => τ e ω) p ds := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.cheapSlope

theorem OAI.GammaFPP.GammaEnvironment.ae_bounded_cost_trail_lengths line 62

Source documentation

On the same probability-one event, every real cost budget bounds the length of all trails starting at any fixed lattice vertex.

theorem GammaEnvironment.ae_bounded_cost_trail_lengths
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ p : Vertex, ∀ M : ℝ, ∃ R : ℕ, ∀ ds : List Step,
      ((trace p ds).map traversalEdge).Nodup →
      pathCost (fun e => τ e ω) p ds ≤ M → ds.length < R := by
…

Mentions: OAI.GammaFPP.GammaEnvironment