OAI/Probability/GammaPassage/ShortCrossingGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.sourceEndpoint line 9
2. theorem OAI.GammaFPP.CrossingBridge.sourceEndpoint_transverse line 11
3. theorem OAI.GammaFPP.CrossingBridge.sourceEndpoint_distance line 18
4. theorem OAI.GammaFPP.CrossingBridge.sourceEndpoint_norm_cost line 32
5. theorem OAI.GammaFPP.CrossingBridge.sourceEndpoint_tube_containment line 48
6. theorem OAI.GammaFPP.CrossingBridge.horizontal_in_crossingRegion line 87

   Source documentation

   For bounded n, a horizontal path suffices; its endpoints need not follow u because E(s,n) leaves the two endpoint columns unrestricted.

   theorem horizontal_in_crossingRegion (b s : ℝ) (n : ℤ) (hb : |b| ≤ 1)
       (hn : 0 ≤ n) (hns : (n : ℝ) ≤ 8*s) :
       PathIn 0 (horizontal n) (rareFastRegion b 1 8 s n 0) := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn, OAI.GammaFPP.CrossingBridge.rareFastRegion