OAI/Combinatorics/BalancedRyser/Local/LocalUsedEventUnion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.UsedEventUnion.UsedWitness line 17
  2. abbrev OAI.Balanced.Local.UsedEventUnion.TripleWitness line 20
  3. def OAI.Balanced.Local.UsedEventUnion.usedConstituentTest line 23
  4. def OAI.Balanced.Local.UsedEventUnion.collinearTest line 30
  5. theorem OAI.Balanced.Local.UsedEventUnion.admissible_usedPairExtra_iff_exists line 45
  6. theorem OAI.Balanced.Local.UsedEventUnion.admissible_forbiddenTriple_imp_exists line 61
  7. theorem OAI.Balanced.Local.UsedEventUnion.conditionedOffsetProbability_exists_le_sum line 71
  8. theorem OAI.Balanced.Local.UsedEventUnion.conditioned_usedPairExtra_le_sum line 81
  9. theorem OAI.Balanced.Local.UsedEventUnion.conditioned_forbiddenTriple_le_sum line 92
  10. def OAI.Balanced.Local.UsedEventUnion.alignedAverage line 104
  11. theorem OAI.Balanced.Local.UsedEventUnion.alignedAverage_mono line 109
  12. theorem OAI.Balanced.Local.UsedEventUnion.alignedAverage_exists_le_sum line 121
  13. theorem OAI.Balanced.Local.UsedEventUnion.card_usedWitness_le line 140
  14. theorem OAI.Balanced.Local.UsedEventUnion.card_tripleWitness line 148
  15. theorem OAI.Balanced.Local.UsedEventUnion.alignedAverage_usedPairExtra_le line 153
  16. theorem OAI.Balanced.Local.UsedEventUnion.alignedAverage_forbiddenTriple_le line 178