OAI/Combinatorics/BalancedRyser/Probability/RootPatternModel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.TupleAlignment.rootSuccessEvent line 19
  2. theorem OAI.Balanced.TupleAlignment.tuplePoint_eq_of_eq_on_generators line 25
  3. abbrev OAI.Balanced.TupleAlignment.rootPatternModel line 35
  4. theorem OAI.Balanced.TupleAlignment.rootPatternModel_support_card line 48
  5. theorem OAI.Balanced.TupleAlignment.rootPatternModel_count line 52
  6. def OAI.Balanced.TupleAlignment.rootOverlapCount line 59
  7. theorem OAI.Balanced.TupleAlignment.rootPatternModel_overlapCount line 64
  8. theorem OAI.Balanced.TupleAlignment.rootPatternModel_measure line 75
  9. theorem OAI.Balanced.TupleAlignment.rootPatternModel_integral line 87
  10. theorem OAI.Balanced.TupleAlignment.rootPatternModel_fixedExpectation line 98
  11. theorem OAI.Balanced.TupleAlignment.rootPatternModel_fixed_count line 106
  12. theorem OAI.Balanced.TupleAlignment.rootPatternModel_fixedExpectation_exposed line 115
  13. theorem OAI.Balanced.TupleAlignment.rootPatternModel_fixed_overlapCount line 130
  14. theorem OAI.Balanced.TupleAlignment.rootPatternModel_fixed_count_exposed line 139