OAI/Probability/GammaPassage/EndpointCoarse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.endpoint_coarse_columns line 9
2. lemma OAI.GammaFPP.CrossingBridge.endpointBox_mono line 24
3. theorem OAI.GammaFPP.CrossingBridge.gridConnections_extend_negative_path line 32

   Source documentation

   Extend a negative-defect path, including one with reversed endpoints, to a positive-span path between coarse columns.

   theorem gridConnections_extend_negative_path (w : Edge → ℝ) (shape rate b m₀ K A R a ε : ℝ)
       (hshape : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (hm : 0 < m₀) (hR : 0 ≤ R) (hε : 0 < ε)
       (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)
       (herror : 2*endpointExtensionError shape rate K k J+2*|a| ≤ ε*(2 : ℝ)^k/2)
       (hscale : (2*R*|a| /m₀)*(2 : ℝ)^k ≤ (gridMesh m J : ℝ))
       (p : Vertex) (ds : List Step) (hin : PathIn p ds (endpointBox b A R k m))
       (hcost : defect w b m₀ a p ds < -ε*(2 : ℝ)^k) :
       ∃ X Y : ℤ, gridMesh m J ∣ X ∧ gridMesh m J ∣ Y ∧
         |(X : ℝ)| ≤ (A+2)*(2 : ℝ)^m ∧ |(Y : ℝ)| ≤ (A+2)*(2 : ℝ)^m ∧
         (gridMesh m J : ℝ) ≤ ((Y-X : ℤ) : ℝ) ∧
         ∃ q es, q.1=X ∧ (q+displacement es).1=Y ∧
   …

   Mentions: OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.endpointExtensionError, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.PathIn, OAI.GammaFPP.CrossingBridge.endpointBox