OAI/Combinatorics/BalancedRyser/Selection/LineOccupancy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.LineOccupancy.transverseHitEquiv line 13
  2. theorem OAI.Balanced.LineOccupancy.transverseHitEquiv_eq_iff line 27
  3. abbrev OAI.Balanced.LineOccupancy.TransverseDirections line 36
  4. theorem OAI.Balanced.LineOccupancy.card_transverseDirections line 39
  5. def OAI.Balanced.LineOccupancy.hitAssignmentsEquiv line 43
  6. def OAI.Balanced.LineOccupancy.unhitCount line 48
  7. theorem OAI.Balanced.LineOccupancy.unhitCount_eq_missedCount line 53
  8. theorem OAI.Balanced.LineOccupancy.unhitCount_eq_filter_card line 64
  9. def OAI.Balanced.LineOccupancy.transverseOffsets line 81
  10. theorem OAI.Balanced.LineOccupancy.unhitCount_eq_initiallyRetained line 84
  11. theorem OAI.Balanced.LineOccupancy.uniformMean_unhitCount line 113
  12. theorem OAI.Balanced.LineOccupancy.integral_unhitCount line 124
  13. theorem OAI.Balanced.LineOccupancy.abs_unhitCount_sub_le_one line 132