OAI/Combinatorics/BalancedRyser/Local/LocalUsedEventMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.UsedEventUnion.injectionAverage line 16
  2. def OAI.Balanced.Local.UsedEventUnion.injectionWeight line 23
  3. theorem OAI.Balanced.Local.UsedEventUnion.injectionWeight_nonneg line 29
  4. theorem OAI.Balanced.Local.UsedEventUnion.injectionWeight_support line 35
  5. theorem OAI.Balanced.Local.UsedEventUnion.injectionAverage_eq_alignedAverage line 40
  6. theorem OAI.Balanced.Local.UsedEventUnion.usedEventMean_eq_injectionAverage line 54
  7. theorem OAI.Balanced.Local.UsedEventUnion.usedEventMean_le_of_test_bounds line 65
  8. theorem OAI.Balanced.Local.UsedEventUnion.pencilTwoReuses_of_injection_test_bounds line 96