OAI/Combinatorics/BalancedRyser/Candidates/CandidateExposure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateExposure.exposedLaw line 14
  2. def OAI.Balanced.CandidateExposure.alignedInDirection line 18
  3. def OAI.Balanced.CandidateExposure.successfulInDirection line 21
  4. def OAI.Balanced.CandidateExposure.conditionalProbability line 24
  5. theorem OAI.Balanced.CandidateExposure.pmf_outer_ne_top line 27
  6. theorem OAI.Balanced.CandidateExposure.pmf_real_mono line 32
  7. theorem OAI.Balanced.CandidateExposure.prescribed_line_probability_le line 37
  8. theorem OAI.Balanced.CandidateExposure.unspecified_line_probability_le_sum line 45
  9. theorem OAI.Balanced.CandidateExposure.unspecified_line_probability_le_of_fixed line 70
  10. theorem OAI.Balanced.CandidateExposure.fixed_positions_table line 97
  11. def OAI.Balanced.CandidateExposure.alignmentExponent line 109
  12. theorem OAI.Balanced.CandidateExposure.alignmentExponent_le_three line 111
  13. theorem OAI.Balanced.CandidateExposure.alignmentExponent_le_nonfixed line 115
  14. theorem OAI.Balanced.CandidateExposure.unspecified_line_probability_le line 122
  15. theorem OAI.Balanced.CandidateExposure.successful_probability_le line 146