OriginEscape.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.IntervalTravelBridge.pathCost_take_le line 10
def OAI.GammaFPP.IntervalTravelBridge.PathIn line 19
Source documentation
Every vertex of a finite path, including the final vertex, is tested.
```
def PathIn (p : Vertex) (ds : List Step) (S : Set Vertex) : Prop :=
…
```
theorem OAI.GammaFPP.IntervalTravelBridge.path_confined_of_escape line 22

theorem OAI.GammaFPP.IntervalTravelBridge.exists_confined_near_optimal line 37

Source documentation

Approximate passage-time minimizers with any positive error bound control the cost of escaping a ball.

theorem exists_confined_near_optimal (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (p q : Vertex) (R a ε : ℝ) (hε : 0 < ε)
    (hescape : ∀ z, R ≤ ‖latticeEmbed (z-p)‖ → a ≤ passageTime w p z)
    (hshort : passageTime w p q + ε ≤ a) :
    ∃ ds, p+displacement ds=q ∧ pathCost w p ds < passageTime w p q+ε ∧
      PathIn p ds {z | ‖latticeEmbed (z-p)‖ < R} := by
…

Mentions: OAI.GammaFPP.IntervalTravelBridge.PathIn

theorem OAI.GammaFPP.IntervalTravelBridge.eventually_escape_of_uniformShape line 48

Source documentation

The origin escape lower bound in cr:local-travel follows from the exact outside-ball estimate. The radius and scale are real, as in the source.

theorem eventually_escape_of_uniformShape (w : Edge → ℝ) (μ : Plane → ℝ)
    (hu : UniformShape w μ) (α δ : ℝ) (hα : 0 < α) (hδ : 0 < δ)
    (hlower : ∀ v, α*‖v‖ ≤ μ v) :
    ∀ᶠ s : ℝ in atTop, ∀ z : Vertex, δ*s/3 ≤ ‖latticeEmbed z‖ →
      α*δ*s/6 ≤ passageTime w 0 z := by
…

theorem OAI.GammaFPP.IntervalTravelBridge.ae_eventually_origin_escape line 69

Source documentation

A lower bound for the Gamma mean norm gives an eventual origin-escape estimate on a probability-one event.

theorem ae_eventually_origin_escape
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (α δ : ℝ) (hα : 0 < α) (hδ : 0 < δ)
    (hlower : ∀ v, α*‖v‖ ≤ gammaMeanNorm h hs hr v) :
    ∀ᵐ ω ∂P, ∀ᶠ s : ℝ in atTop, ∀ z : Vertex,
      δ*s/3 ≤ ‖latticeEmbed z‖ → α*δ*s/6 ≤ passageTime (fun e => τ e ω) 0 z := by
…

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