OAI/Combinatorics/BalancedRyser/Local/PartialAlignment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.PartialAlignment.PartialOffsets line 10
  2. def OAI.Balanced.PartialAlignment.freshGenerators line 13
  3. def OAI.Balanced.PartialAlignment.freePositions line 16
  4. def OAI.Balanced.PartialAlignment.fixedPositions line 19
  5. def OAI.Balanced.PartialAlignment.partialFreshEquiv line 22
  6. theorem OAI.Balanced.PartialAlignment.alignment_exponent_identity line 39
  7. abbrev OAI.Balanced.PartialAlignment.AlignedPartialOffsets line 49
  8. def OAI.Balanced.PartialAlignment.alignedFreeCoordinates line 55
  9. theorem OAI.Balanced.PartialAlignment.alignedFreeCoordinates_injective line 62
  10. instance OAI.Balanced.PartialAlignment.(instance at line 93) line 93
  11. theorem OAI.Balanced.PartialAlignment.card_partialOffsets line 100
  12. theorem OAI.Balanced.PartialAlignment.card_alignedPartialOffsets_le line 107
  13. theorem OAI.Balanced.PartialAlignment.partial_alignment_probability_le line 120
  14. theorem OAI.Balanced.PartialAlignment.partialOffsets_supported line 148
  15. theorem OAI.Balanced.PartialAlignment.partialOffsets_conditional_law line 153
  16. theorem OAI.Balanced.PartialAlignment.original_conditional_alignment_probability_le line 161