EndpointBlocks.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Path blocks supplied by the simultaneous grid event.

theorem OAI.GammaFPP.CrossingBridge.gridConnections_block line 13

Source documentation

A row of n adjacent grid intervals, with the same transverse target at all joining columns. Costs charge every traversal; all vertices are retained.

theorem gridConnections_block (w : Edge → ℝ) (shape rate b m₀ K A R H : ℝ)
    (hs : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (hH : 1 ≤ H) (k m J : ℕ) (hJ : 1 ≤ J)
    (hg : w ∈ gridConnectionsEvent shape rate b m₀ K A R k m J)
    (j : ℕ) (hj : J ≤ j ∧ j ≤ gridLastLevel m)
    (he : (Grid.attachmentAllowance shape rate K)*(j : ℝ)^2*(gridWidth k j) ≤ H)
    (X : ℤ) (hX : gridMesh m j ∣ X) (n : ℕ)
    (hlo : -(A+4)*(2 : ℝ)^m ≤ (X : ℝ))
    (hhi : ((X+(n : ℤ)*gridMesh m j : ℤ) : ℝ) ≤ (A+4)*(2 : ℝ)^m)
    (r : ℝ) (hr : |r| ≤ R*(2 : ℝ)^k) :
    ∃ ds, endpointVertex b r X+displacement ds=
        endpointVertex b r (X+(n : ℤ)*gridMesh m j) ∧
      pathCost w (endpointVertex b r X) ds ≤
…

Mentions: OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.Grid.attachmentAllowance, OAI.GammaFPP.CrossingBridge.gridWidth, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.endpointVertex