OAI/Combinatorics/BalancedRyser/Selection/SelectionSourceConcentration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Selection.Process.sourceDegreeCensorBound line 13
  2. theorem OAI.Balanced.Selection.Process.postcheckTail_nonneg_of_admissible line 17
  3. theorem OAI.Balanced.Selection.Process.sourceDegreeCensorBound_nonneg line 24
  4. theorem OAI.Balanced.Selection.Process.eventually_small_power_error line 33
  5. theorem OAI.Balanced.Selection.Process.tendsto_domain_drift_budget line 57
  6. theorem OAI.Balanced.Selection.Process.eventually_source_drift_budgets line 65
  7. theorem OAI.Balanced.Selection.Process.card_vertices_le_slots_mul_order line 98
  8. theorem OAI.Balanced.Selection.Process.source_track_tail_sum_le_error line 110
  9. theorem OAI.Balanced.Selection.Process.source_true_count_failure_probability_le line 156
  10. theorem OAI.Balanced.Selection.Process.exists_source_concentration_threshold line 202