EndpointConnection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.CrossingBridge.ColumnConnection line 10
Source documentation
A localized finite path between fixed-target lattice vertices.
```
def ColumnConnection (w : Edge → ℝ) (b r m₀ E : ℝ) (S : Set Vertex) (X Y : ℤ) : Prop :=
…
```
lemma OAI.GammaFPP.CrossingBridge.ColumnConnection.mono line 15
lemma OAI.GammaFPP.CrossingBridge.ColumnConnection.trans line 21
def OAI.GammaFPP.CrossingBridge.endpointTube line 33

lemma OAI.GammaFPP.CrossingBridge.gridConnections_block_connection line 38

Source documentation

Coarsened path blocks for the entrance and exit constructions on the simultaneous grid event.

lemma gridConnections_block_connection (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 Y B T : ℤ) (hX : gridMesh m j ∣ X) (n : ℕ) (hn : n ≤ 16)
    (hXY : X+(n : ℤ)*gridMesh m j=Y)
    (hlo : -(A+4)*(2 : ℝ)^m ≤ (X : ℝ))
    (hhi : (Y : ℝ) ≤ (A+4)*(2 : ℝ)^m)
    (hB : B ≤ X-gridMesh m j) (hT : Y+gridMesh m j ≤ T)
    (r : ℝ) (hr : |r| ≤ R*(2 : ℝ)^k) :
    ColumnConnection w b r m₀ (16*((Grid.attachmentAllowance shape rate K)*(j : ℝ)^2*gridWidth k j))
…

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