OAI/Combinatorics/Ryser/LineCover/FailureNumerics.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.LineCover.lowFailureEnvelope line 13
  2. def OAI.RyserCoveringCounterexample.LineCover.highFailureEnvelope line 22
  3. theorem OAI.RyserCoveringCounterexample.LineCover.low_occupancy_decay_pos line 31
  4. theorem OAI.RyserCoveringCounterexample.LineCover.high_occupancy_decay_pos line 39
  5. theorem OAI.RyserCoveringCounterexample.LineCover.tendsto_lowFailureEnvelope_atTop line 46
  6. theorem OAI.RyserCoveringCounterexample.LineCover.tendsto_highFailureEnvelope_atTop line 65
  7. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_lowFailureEnvelope_lt_one line 80
  8. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_highFailureEnvelope_lt_one line 86
  9. theorem OAI.RyserCoveringCounterexample.LineCover.low_concurrency_ratio_le line 92
  10. theorem OAI.RyserCoveringCounterexample.LineCover.high_concurrency_inverse_le line 106
  11. theorem OAI.RyserCoveringCounterexample.LineCover.sampling_occupancy_le_power line 114
  12. theorem OAI.RyserCoveringCounterexample.LineCover.high_survivor_term_le line 138
  13. theorem OAI.RyserCoveringCounterexample.LineCover.low_coarse_failure_le_envelope line 166
  14. theorem OAI.RyserCoveringCounterexample.LineCover.high_coarse_failure_le_envelope line 220
  15. theorem OAI.RyserCoveringCounterexample.LineCover.low_sampling_failure_le_envelope line 259
  16. theorem OAI.RyserCoveringCounterexample.LineCover.high_sampling_failure_le_envelope line 277
  17. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_sampleSize_le_mul_rpow line 299
  18. theorem OAI.RyserCoveringCounterexample.LineCover.eventually_sampling_size_bounds line 308