OAI/Combinatorics/BalancedRyser/Local/ReuseTargetSum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.PartialAlignment.externalAlignmentEvent line 15
  2. def OAI.Balanced.PartialAlignment.externalAlignmentProbability line 22
  3. theorem OAI.Balanced.PartialAlignment.externalAlignmentProbability_le line 29
  4. theorem OAI.Balanced.PartialAlignment.tuplePosition_fixed line 50
  5. def OAI.Balanced.PartialAlignment.possibleExternalTargets line 58
  6. theorem OAI.Balanced.PartialAlignment.card_possibleExternalTargets_le_one line 64
  7. theorem OAI.Balanced.PartialAlignment.externalAlignmentProbability_eq_zero_of_not_possible line 81
  8. theorem OAI.Balanced.PartialAlignment.sum_externalAlignmentProbability_le line 93
  9. theorem OAI.Balanced.PartialAlignment.fixedPositions_eq_fixedGeneratorPositions line 131
  10. theorem OAI.Balanced.PartialAlignment.scaled_sum_externalAlignmentProbability_le line 136