OAI/Probability/GammaPassage/GridCounting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite supersets of grid intervals and transverse bins, with cardinality bounds independent of the characteristic scale.

  1. def OAI.GammaFPP.CrossingBridge.gridIndexRange line 11
  2. lemma OAI.GammaFPP.CrossingBridge.gridIndexRange_card line 14
  3. lemma OAI.GammaFPP.CrossingBridge.mem_gridIndexRange_of_abs_le line 18
  4. def OAI.GammaFPP.CrossingBridge.gridTestIndices line 24
  5. def OAI.GammaFPP.CrossingBridge.gridIndexConstant line 27
  6. lemma OAI.GammaFPP.CrossingBridge.gridIndexConstant_pos line 30
  7. lemma OAI.GammaFPP.CrossingBridge.gridTestIndices_card line 33
  8. lemma OAI.GammaFPP.CrossingBridge.gridTestIndices_level_card line 52
  9. lemma OAI.GammaFPP.CrossingBridge.grid_interval_index_mem line 77
  10. lemma OAI.GammaFPP.CrossingBridge.grid_bin_floor line 101