EndpointExit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.gridConnections_exit_levels line 11

Source documentation

Reflected mesh subdivision, concatenated from left to right with the same edge weights and simultaneous grid event.

theorem gridConnections_exit_levels (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)
    (herr : ∀ j, J ≤ j → j ≤ gridLastLevel m → (Grid.attachmentAllowance shape rate K)*(j : ℝ)^2*gridWidth k j ≤ H)
    (x : ℤ) (hlo : -(A+4)*(2 : ℝ)^m ≤ (x : ℝ))
    (hhi : (exitColumn x m J : ℝ) ≤ (A+4)*(2 : ℝ)^m)
    (r : ℝ) (hr : |r| ≤ R*(2 : ℝ)^k) (n : ℕ) (hn : J+n ≤ gridLastLevel m) :
    ColumnConnection w b r m₀
      (∑ i ∈ range (n+1),16*((Grid.attachmentAllowance shape rate K)*((J+i : ℕ) : ℝ)^2*gridWidth k (J+i)))
      (endpointTube b r H (x-gridMesh m J) (exitColumn x m J+gridMesh m J))
      (-endpointColumn (-x) m (J+n)) (exitColumn x m J) := by
…

Mentions: OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.Grid.attachmentAllowance, OAI.GammaFPP.CrossingBridge.gridWidth, OAI.GammaFPP.CrossingBridge.exitColumn, OAI.GammaFPP.CrossingBridge.ColumnConnection, OAI.GammaFPP.CrossingBridge.endpointTube, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.endpointColumn

theorem OAI.GammaFPP.CrossingBridge.gridConnections_exit line 65

Source documentation

The exit path reaches the coarse right column.

theorem gridConnections_exit (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) (hlast : J ≤ gridLastLevel m)
    (hg : w ∈ gridConnectionsEvent shape rate b m₀ K A R k m J)
    (herr : ∀ j, J ≤ j → j ≤ gridLastLevel m → (Grid.attachmentAllowance shape rate K)*(j : ℝ)^2*gridWidth k j ≤ H)
    (p : Vertex) (hlo : -(A+4)*(2 : ℝ)^m ≤ (p.1 : ℝ))
    (hhi : (exitColumn p.1 m J : ℝ) ≤ (A+4)*(2 : ℝ)^m) (hr : |transverse b p| ≤ R*(2 : ℝ)^k) :
    ∃ ds, p+displacement ds=endpointVertex b (transverse b p) (exitColumn p.1 m J) ∧
      pathCost w p ds ≤ m₀*((exitColumn p.1 m J-p.1 : ℤ) : ℝ)+
        ∑ i ∈ range (gridLastLevel m-J+1),16*((Grid.attachmentAllowance shape rate K)*((J+i : ℕ) : ℝ)^2*gridWidth k (J+i)) ∧
      PathIn p ds (endpointTube b (transverse b p) H (p.1-gridMesh m J) (exitColumn p.1 m J+gridMesh m J)) := by
…

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