PassageLowerBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.displacement_natAbs_sum_le_length line 13
Source documentation
Each original nearest-neighbor step contributes at most one L1 unit.
```
lemma displacement_natAbs_sum_le_length (ds : List Step) :
    (displacement ds).1.natAbs + (displacement ds).2.natAbs ≤ ds.length := by
…
```

lemma OAI.GammaFPP.latticeDistance_endpoint_le_length line 28

Source documentation

Literal latticeDistance, not the product max norm.

lemma latticeDistance_endpoint_le_length (p : Vertex) (ds : List Step) :
    latticeDistance p (p + displacement ds) ≤ ds.length := by
…

lemma OAI.GammaFPP.pathCost_lower_of_long_trails line 35

Source documentation

Erasure preserves the endpoint, so every sufficiently distant arbitrary path inherits the long-trail lower bound, even if it repeats edges.

lemma pathCost_lower_of_long_trails (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (c : ℝ) (hc : 0 ≤ c) (p : Vertex) (N : ℕ)
    (hN : ∀ es : List Step, N ≤ es.length →
      ((trace p es).map traversalEdge).Nodup → c * (es.length : ℝ) < pathCost w p es)
    (q : Vertex) (hq : N ≤ latticeDistance p q) (ds : List Step)
    (hend : p + displacement ds = q) :
    c * (latticeDistance p q : ℝ) < pathCost w p ds := by
…

lemma OAI.GammaFPP.passageTime_lower_of_long_trails line 53

Source documentation

Taking the infimum of path costs preserves the non-strict lower bound, without requiring the existence of a minimizing path.

lemma passageTime_lower_of_long_trails (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (c : ℝ) (hc : 0 ≤ c) (p : Vertex) (N : ℕ)
    (hN : ∀ es : List Step, N ≤ es.length →
      ((trace p es).map traversalEdge).Nodup → c * (es.length : ℝ) < pathCost w p es)
    (q : Vertex) (hq : N ≤ latticeDistance p q) :
    c * (latticeDistance p q : ℝ) ≤ passageTime w p q := by
…

theorem OAI.GammaFPP.GammaEnvironment.ae_all_starts_passageTime_lower line 68

Source documentation

On one probability-one event, every lattice start has an eventual metric lower bound for all distant endpoints. The cutoff may depend on start/sample.

theorem GammaEnvironment.ae_all_starts_passageTime_lower
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    ∀ᵐ ω ∂P, ∀ p : Vertex, ∃ N : ℕ, ∀ q : Vertex,
      N ≤ latticeDistance p q →
        cheapSlope shape rate * (latticeDistance p q : ℝ) ≤
          passageTime (fun e => τ e ω) p q := by
…

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