OAI/Combinatorics/BalancedRyser/Probability/NearCoverFinite.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.NearCoverVisibility.sum_le_tolerance_card_add_bad line 13
  2. theorem OAI.Balanced.NearCoverVisibility.occupancy_deviation_le_one line 35
  3. theorem OAI.Balanced.NearCoverVisibility.empirical_absolute_row_deviation_le line 56
  4. theorem OAI.Balanced.NearCoverVisibility.nearCoverClass_integral_abs_tendsto line 91
  5. theorem OAI.Balanced.NearCoverVisibility.empiricalMultiplicityMass_zero line 107
  6. theorem OAI.Balanced.NearCoverVisibility.core_density_error_le_twice_tv line 118
  7. theorem OAI.Balanced.NearCoverVisibility.nearCoverClass_sizeGap line 136
  8. theorem OAI.Balanced.NearCoverVisibility.nearCoverClass_core_density_tendsto line 151
  9. theorem OAI.Balanced.NearCoverVisibility.nearCoverClass_limit_corner_budget line 167