OAI/Combinatorics/BalancedRyser/Local/LocalTwoReuseUsedEvents.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.TwoReuseAssembly.unused_errors_le line 10
  2. theorem OAI.Balanced.Local.TwoReuseAssembly.mean_le_mean_add line 28
  3. def OAI.Balanced.Local.TwoReuseAssembly.usedEventConditionalMass line 41
  4. def OAI.Balanced.Local.TwoReuseAssembly.usedEventMean line 48
  5. theorem OAI.Balanced.Local.TwoReuseAssembly.badCover_mean_le_usedEventMean line 53
  6. def OAI.Balanced.Local.TwoReuseAssembly.InjectiveUsedEventsEstimate line 76
  7. theorem OAI.Balanced.Local.TwoReuseAssembly.pencilTwoReuses_of_used_event_mean line 83