EndpointGeometry.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed transverse targets and whole-extension support errors for gr:variable-endpoints. Rounding is charged once, independently of levels.

theorem OAI.GammaFPP.CrossingBridge.exists_path_chain line 15

Source documentation

Concatenate a finite deterministic list of connections, retaining every vertex-localization condition and adding their actual traversal costs.

theorem exists_path_chain (w : Edge → ℝ) (p : ℕ → Vertex) (S : Set Vertex)
    (a : ℕ → ℝ) (n : ℕ) (hp : p 0 ∈ S)
    (h : ∀ i < n, ∃ ds, p i+displacement ds=p (i+1) ∧
      pathCost w (p i) ds ≤ a i ∧ PathIn (p i) ds S) :
    ∃ ds, p 0+displacement ds=p n ∧
      pathCost w (p 0) ds ≤ ∑ i ∈ range n, a i ∧ PathIn (p 0) ds S := by
…

Mentions: OAI.GammaFPP.CrossingBridge.PathIn

def OAI.GammaFPP.CrossingBridge.endpointVertex line 37
lemma OAI.GammaFPP.CrossingBridge.endpointVertex_error line 39
lemma OAI.GammaFPP.CrossingBridge.endpointVertex_close line 47
lemma OAI.GammaFPP.CrossingBridge.endpointVertex_self line 52
lemma OAI.GammaFPP.CrossingBridge.endpointVertex_displacement line 58
lemma OAI.GammaFPP.CrossingBridge.endpoint_path_defect line 68

lemma OAI.GammaFPP.CrossingBridge.negative_defect_reverse_span line 88

Source documentation

Reverse-displacement estimate for a negative-defect path, allowing unordered endpoints.

lemma negative_defect_reverse_span (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (b m₀ a R s ε : ℝ) (hm : 0 < m₀) (_hR : 0 ≤ R) (hs : 0 ≤ s) (hε : 0 ≤ ε)
    (p z : Vertex) (ds : List Step) (hd : p+displacement ds=z)
    (hp : |transverse b p| ≤ R*s) (hz : |transverse b z| ≤ R*s)
    (hc : defect w b m₀ a p ds < -ε*s) :
    -2*R*|a| *s/m₀ ≤ ((z.1-p.1 : ℤ) : ℝ) := by
…

lemma OAI.GammaFPP.CrossingBridge.extended_columns_span line 112