EndpointEntrance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.gridConnections_entrance_levels line 11

Source documentation

Complete greedy entrance through level J+n. At n=j*-J its endpoint is exactly x, and each level is charged at most sixteen times.

theorem gridConnections_entrance_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 ≤ (entranceColumn x m J : ℝ))
    (hhi : (x : ℝ) ≤ (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 (entranceColumn x m J-gridMesh m J) (x+gridMesh m J))
      (entranceColumn x m J) (endpointColumn x m (J+n)) := by
…

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

theorem OAI.GammaFPP.CrossingBridge.gridConnections_entrance line 60

Source documentation

Entrance path obtained by greedy mesh subdivision.

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

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