OAI/Combinatorics/Ryser/Construction/GadgetProcess.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Construction.nonzeroSlope_card line 19
  2. def OAI.RyserCoveringCounterexample.Construction.cubicTrialLaw line 24
  3. theorem OAI.RyserCoveringCounterexample.Construction.cubicTrialLaw_point_probability line 28
  4. theorem OAI.RyserCoveringCounterexample.Construction.cubicTrialLaw_point_probability_le line 43
  5. theorem OAI.RyserCoveringCounterexample.Construction.cubicTrialLaw_line_probability_zero line 51
  6. def OAI.RyserCoveringCounterexample.Construction.gadgetSlope line 61
  7. def OAI.RyserCoveringCounterexample.Construction.gadgetTrials line 64
  8. def OAI.RyserCoveringCounterexample.Construction.gadgetSurvival line 68
  9. theorem OAI.RyserCoveringCounterexample.Construction.gadgetTrials_uniformSurvival line 71
  10. def OAI.RyserCoveringCounterexample.Construction.gadgetDeletionProcess line 83
  11. theorem OAI.RyserCoveringCounterexample.Construction.gadgetDeletionProcess_trialsCount line 108
  12. def OAI.RyserCoveringCounterexample.Construction.cubicDeletionProcess line 114
  13. def OAI.RyserCoveringCounterexample.Construction.primeCubicDeletionProcess line 120
  14. def OAI.RyserCoveringCounterexample.Construction.gadgetLaw line 126
  15. def OAI.RyserCoveringCounterexample.Construction.gadgetInterceptEquiv line 130
  16. def OAI.RyserCoveringCounterexample.Construction.gadgetConfig line 141
  17. theorem OAI.RyserCoveringCounterexample.Construction.gadgetLaw_map_config line 145
  18. theorem OAI.RyserCoveringCounterexample.Construction.gadgetConfig_survivors line 161
  19. theorem OAI.RyserCoveringCounterexample.Construction.gadgetLaw_transformedRetained_probability line 178