OAI/Combinatorics/Ryser/Incidence/Parameters.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Incidence.savingExponent line 13
  2. def OAI.RyserCoveringCounterexample.Incidence.witnessConstant line 14
  3. def OAI.RyserCoveringCounterexample.Incidence.graphScaleConstant line 15
  4. def OAI.RyserCoveringCounterexample.Incidence.densityScale line 16
  5. def OAI.RyserCoveringCounterexample.Incidence.graphScale line 17
  6. def OAI.RyserCoveringCounterexample.Incidence.expansionScale line 18
  7. theorem OAI.RyserCoveringCounterexample.Incidence.savingExponent_pos line 20
  8. theorem OAI.RyserCoveringCounterexample.Incidence.savingExponent_lt_tenth line 22
  9. theorem OAI.RyserCoveringCounterexample.Incidence.witnessConstant_pos line 24
  10. theorem OAI.RyserCoveringCounterexample.Incidence.graphScaleConstant_pos line 26
  11. theorem OAI.RyserCoveringCounterexample.Incidence.graphScaleConstant_eq line 28
  12. theorem OAI.RyserCoveringCounterexample.Incidence.graphScale_pos line 31
  13. theorem OAI.RyserCoveringCounterexample.Incidence.expansionScale_pos line 33
  14. theorem OAI.RyserCoveringCounterexample.Incidence.scaled_power_identity line 36
  15. theorem OAI.RyserCoveringCounterexample.Incidence.eventually_coefficient_density_power_lt_sqrt line 44
  16. theorem OAI.RyserCoveringCounterexample.Incidence.eventually_scaled_powers_lt_sqrt line 58
  17. def OAI.RyserCoveringCounterexample.Incidence.LargeEnough line 69
  18. theorem OAI.RyserCoveringCounterexample.Incidence.eventually_largeEnough line 81
  19. theorem OAI.RyserCoveringCounterexample.Incidence.exists_threshold_largeEnough line 106
  20. def OAI.RyserCoveringCounterexample.Incidence.incidenceThreshold line 112
  21. theorem OAI.RyserCoveringCounterexample.Incidence.largeEnough_of_threshold line 114