OAI/Combinatorics/BalancedRyser/Incidence/PartialIncidence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PartialAlignment.card_fixed_function_coordinate line 14
  2. abbrev OAI.Balanced.PartialAlignment.MarkedPartialOffsets line 23
  3. theorem OAI.Balanced.PartialAlignment.card_markedPartialOffsets_le line 31
  4. theorem OAI.Balanced.PartialAlignment.partial_marked_alignment_probability_le line 65
  5. theorem OAI.Balanced.PartialAlignment.original_conditional_marked_alignment_probability_le line 98
  6. theorem OAI.Balanced.PartialAlignment.canonical_conditional_marked_alignment_probability_le line 111
  7. theorem OAI.Balanced.PartialAlignment.canonical_conditional_transverse_hit_probability_le line 135
  8. theorem OAI.Balanced.PartialAlignment.pmf_outer_ne_top line 166
  9. theorem OAI.Balanced.PartialAlignment.pmf_real_mono line 174
  10. def OAI.Balanced.PartialAlignment.conditionalHitProbability line 178
  11. theorem OAI.Balanced.PartialAlignment.conditionalHitProbability_le_alignment line 184
  12. def OAI.Balanced.PartialAlignment.possibleHitOffsets line 193
  13. theorem OAI.Balanced.PartialAlignment.card_possibleHitOffsets_le_one line 199
  14. theorem OAI.Balanced.PartialAlignment.conditionalHitProbability_eq_zero_of_not_possible line 243
  15. theorem OAI.Balanced.PartialAlignment.fixedPositions_card_zero_of_le_one line 260
  16. theorem OAI.Balanced.PartialAlignment.sum_conditionalHitProbability_le line 265
  17. theorem OAI.Balanced.PartialAlignment.pmf_real_iUnion_le line 309
  18. theorem OAI.Balanced.PartialAlignment.sum_conditional_any_hit_probability_le line 319
  19. theorem OAI.Balanced.PartialAlignment.canonical_conditional_one_exposed_hit_probability_le line 356