OAI/Probability/GammaPassage/EndpointBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.gridMesh_le_scale line 10
2. lemma OAI.GammaFPP.CrossingBridge.grid_endpoint_height line 16
3. def OAI.GammaFPP.CrossingBridge.endpointExtensionError line 25
4. lemma OAI.GammaFPP.CrossingBridge.endpoint_extension_cost_sum line 28
5. lemma OAI.GammaFPP.CrossingBridge.endpoint_localization line 49

   Source documentation

   Localized attachment vertices stay in the manuscript's enlarged box.

   lemma endpoint_localization (b A R C : ℝ) (_hC : 0 ≤ C) (k m : ℕ) (p z : Vertex) (d : ℤ)
       (hd : (d : ℝ) ≤ (2 : ℝ)^m)
       (hp : |(p.1 : ℝ)| ≤ A*(2 : ℝ)^m) (hr : |transverse b p| ≤ R*(2 : ℝ)^k)
       (hx : p.1-3*d ≤ z.1 ∧ z.1 ≤ p.1+3*d)
       (hz : |transverse b z-transverse b p| ≤ 2*C*(2 : ℝ)^k) :
       |(z.1 : ℝ)| ≤ (A+4)*(2 : ℝ)^m ∧
         |transverse b z| ≤ (R+2*C)*(2 : ℝ)^k := by
   …