OAI/Probability/GammaPassage/SpatialChunkGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.spatialChunkIndex line 8
2. lemma OAI.GammaFPP.CrossingBridge.spatialTranslate_center line 11
3. lemma OAI.GammaFPP.CrossingBridge.spatialChunkIndex_horizontal line 17
4. lemma OAI.GammaFPP.CrossingBridge.spatialChunkIndex_transverse line 24
5. lemma OAI.GammaFPP.CrossingBridge.spatial_chunk_vertex_in_box line 38

   Source documentation

   Source chunk localization, including the possible one-unit transverse overshoot at the first exit.

   lemma spatial_chunk_vertex_in_box (b : ℝ) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k) (p z : Vertex)
       (hx : |z.1-p.1| ≤ 2*(2 : ℤ)^m)
       (hr : |transverse b z-transverse b p| ≤ (2 : ℝ)^k+1) :
       z-spatialTranslate b k m (spatialChunkIndex b k m p) ∈ endpointBox b 4 4 k m := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.spatialTranslate, OAI.GammaFPP.CrossingBridge.spatialChunkIndex, OAI.GammaFPP.CrossingBridge.endpointBox

6. lemma OAI.GammaFPP.CrossingBridge.spatial_chunk_in_box line 61
7. lemma OAI.GammaFPP.CrossingBridge.spatialChunkIndex_origin line 70
8. lemma OAI.GammaFPP.CrossingBridge.spatialChunkIndex_increment line 75

   Source documentation

   Consecutive source chunk indices have coordinate increments at most 3, so a length-N itinerary has at most 49 choices at each step.

   lemma spatialChunkIndex_increment (b : ℝ) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k) (p z : Vertex)
       (hx : |z.1-p.1| ≤ 2*(2 : ℤ)^m)
       (hr : |transverse b z-transverse b p| ≤ (2 : ℝ)^k+1) :
       |(spatialChunkIndex b k m z).1-(spatialChunkIndex b k m p).1| ≤ 3 ∧
         |(spatialChunkIndex b k m z).2-(spatialChunkIndex b k m p).2| ≤ 3 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.spatialChunkIndex