OAI/Combinatorics/Ryser/Selection/CertificateBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.smallCertificateBase line 12
  2. def OAI.RyserCoveringCounterexample.Selection.densityFailureBound line 15
  3. def OAI.RyserCoveringCounterexample.Selection.certificateEventBound line 18
  4. theorem OAI.RyserCoveringCounterexample.Selection.certificateEventBound_nonneg line 23
  5. theorem OAI.RyserCoveringCounterexample.Selection.smallCertificateBase_eq line 28
  6. theorem OAI.RyserCoveringCounterexample.Selection.smallCertificateBase_le_half line 33
  7. theorem OAI.RyserCoveringCounterexample.Selection.exists_threshold_certificate_event_bound line 51