OAI/Combinatorics/Ryser/LineCover/RigidityNumerics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.LineCover.rigidityBudget line 12
  2. theorem OAI.RyserCoveringCounterexample.LineCover.rigidityBudget_eq_errors line 15
  3. theorem OAI.RyserCoveringCounterexample.LineCover.rigidityBudget_nonneg line 27
  4. theorem OAI.RyserCoveringCounterexample.LineCover.rigidityBudget_le line 32
  5. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_mul_rpow_le_mul line 43
  6. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_rigidityBudget_div_le line 58
  7. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_rigidityBudget_div_le_min line 72
  8. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_rigidity_heavy_bounds line 80
  9. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_line_error_le_half line 106
  10. theorem OAI.RyserCoveringCounterexample.LineCover.pair_mass_ratio_le_coarse line 117
  11. theorem OAI.RyserCoveringCounterexample.LineCover.rigidity_pair_ratio_le line 157