EndpointExtensions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Whole entrance and exit paths for Lemma gr:variable-endpoints.

def OAI.GammaFPP.CrossingBridge.endpointBox line 12

theorem OAI.GammaFPP.CrossingBridge.gridConnections_endpoint_extensions line 17

Source documentation

Entrance and exit extensions with cost and enlarged-localization bounds, simultaneously for every lattice vertex in the box.

theorem gridConnections_endpoint_extensions (w : Edge → ℝ) (shape rate b m₀ K A R : ℝ)
    (hshape : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (k m J : ℕ) (hJ : 1 ≤ J) (hJlast : J ≤ gridLastLevel m)
    (hlast : gridLastLevel m ≤ k)
    (hg : w ∈ gridConnectionsEvent shape rate b m₀ K A R k m J)
    (p : Vertex) (hp : p ∈ endpointBox b A R k m) :
    ColumnConnection w b (transverse b p) m₀ (endpointExtensionError shape rate K k J)
      (endpointBox b (A+4) (R+2*(Grid.attachmentAllowance shape rate K)) k m) (entranceColumn p.1 m J) p.1 ∧
    ColumnConnection w b (transverse b p) m₀ (endpointExtensionError shape rate K k J)
      (endpointBox b (A+4) (R+2*(Grid.attachmentAllowance shape rate K)) k m) p.1 (exitColumn p.1 m J) := by
…

Mentions: OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.endpointBox, OAI.GammaFPP.CrossingBridge.ColumnConnection, OAI.GammaFPP.CrossingBridge.endpointExtensionError, OAI.GammaFPP.Grid.attachmentAllowance, OAI.GammaFPP.CrossingBridge.entranceColumn, OAI.GammaFPP.CrossingBridge.exitColumn

theorem OAI.GammaFPP.CrossingBridge.gridConnections_endpoint_defects line 79

Source documentation

Defect bounds for either supporting slope. The fixed-target floor error is paid once for each whole attachment.

theorem gridConnections_endpoint_defects (w : Edge → ℝ) (shape rate b m₀ K A R : ℝ)
    (hshape : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (k m J : ℕ) (hJ : 1 ≤ J) (hJlast : J ≤ gridLastLevel m)
    (hlast : gridLastLevel m ≤ k)
    (hg : w ∈ gridConnectionsEvent shape rate b m₀ K A R k m J)
    (p : Vertex) (hp : p ∈ endpointBox b A R k m) :
    ∃ ds es,
      endpointVertex b (transverse b p) (entranceColumn p.1 m J)+displacement ds=p ∧
      p+displacement es=endpointVertex b (transverse b p) (exitColumn p.1 m J) ∧
      (∀ a : ℝ, defect w b m₀ a (endpointVertex b (transverse b p) (entranceColumn p.1 m J)) ds ≤
        endpointExtensionError shape rate K k J+|a|) ∧
      (∀ a : ℝ, defect w b m₀ a p es ≤ endpointExtensionError shape rate K k J+|a|) ∧
      PathIn (endpointVertex b (transverse b p) (entranceColumn p.1 m J)) ds
…

Mentions: OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.endpointBox, OAI.GammaFPP.CrossingBridge.endpointVertex, OAI.GammaFPP.CrossingBridge.entranceColumn, OAI.GammaFPP.CrossingBridge.exitColumn, OAI.GammaFPP.CrossingBridge.endpointExtensionError, OAI.GammaFPP.CrossingBridge.PathIn