OAI/Probability/GammaPassage/TiltRegionCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.int_interval_card_real_le line 8
2. def OAI.GammaFPP.CrossingBridge.tiltColumn line 22
3. theorem OAI.GammaFPP.CrossingBridge.tiltColumn_card line 25
4. theorem OAI.GammaFPP.CrossingBridge.rareFast_tilt_vertices_card line 31
5. theorem OAI.GammaFPP.CrossingBridge.rareFast_tilt_edges_card line 69

   Source documentation

   The internal-edge count is at most 144 * n * s, for every lattice phase.

   theorem rareFast_tilt_edges_card (b s : ℝ) (n : ℤ) (hs : 1 ≤ s) (hn : 1 ≤ n) :
       ((internalEdges (rareFastVertices b 1 8 s n 0)).card : ℝ) ≤ 144*(n : ℝ)*s := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.internalEdges, OAI.GammaFPP.CrossingBridge.rareFastVertices