OAI/Probability/GammaPassage/SpatialFirstExit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.chunkInterior line 8
2. def OAI.GammaFPP.CrossingBridge.FullSpatialChunk line 11
3. lemma OAI.GammaFPP.CrossingBridge.chunkInterior_zero line 15
4. lemma OAI.GammaFPP.CrossingBridge.fullSpatialChunk_nonempty line 21
5. theorem OAI.GammaFPP.CrossingBridge.first_full_spatial_chunk line 29

   Source documentation

   The first exit is selected from the actual finite path. No chunk or subpath existence is assumed.

   theorem first_full_spatial_chunk (b : ℝ) (k m : ℕ) (ds : List Step) :
       (∀ i ≤ ds.length, chunkInterior b k m (displacement (ds.take i))) ∨
       ∃ pre rest : List Step, ds=pre++rest ∧ pre ≠ [] ∧ FullSpatialChunk b k m pre := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.chunkInterior, OAI.GammaFPP.CrossingBridge.FullSpatialChunk

6. lemma OAI.GammaFPP.CrossingBridge.step_transverse_abs_le line 57
7. lemma OAI.GammaFPP.CrossingBridge.chunk_step_localization line 66

   Source documentation

   A step out of the open chunk rectangle overshoots transversely by at most one and cannot overshoot the integer longitudinal boundary.

   lemma chunk_step_localization (b : ℝ) (hb : |b| ≤ 1) (k m : ℕ) (v : Vertex)
       (hv : chunkInterior b k m v) (d : Step) :
       |(v+d.delta).1| ≤ 2*(2 : ℤ)^m ∧ |transverse b (v+d.delta)| ≤ (2 : ℝ)^k+1 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.chunkInterior

8. lemma OAI.GammaFPP.CrossingBridge.proper_chunk_endpoint_localization line 75
9. lemma OAI.GammaFPP.CrossingBridge.proper_chunk_localization line 90
10. lemma OAI.GammaFPP.CrossingBridge.fullSpatialChunk_in_box line 101

    Source documentation

    Every full first-exit chunk supplies the precise spatial box needed by the actual witness family, including its terminal vertex.

    lemma fullSpatialChunk_in_box (b : ℝ) (hb : |b| ≤ 1) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
        (p : Vertex) (ds : List Step) (h : FullSpatialChunk b k m ds) :
        PathIn p ds {z | z-spatialTranslate b k m (spatialChunkIndex b k m p) ∈ endpointBox b 4 4 k m} :=
    …

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