OAI/Combinatorics/BalancedRyser/Candidates/CandidateMixedExternal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateMixedExternal.tupleTarget line 18
  2. theorem OAI.Balanced.CandidateMixedExternal.successful_on_tupleTarget line 22
  3. def OAI.Balanced.CandidateMixedExternal.mixedExternalEvent line 29
  4. theorem OAI.Balanced.CandidateMixedExternal.mixedExternalEvent_symm line 38
  5. def OAI.Balanced.CandidateMixedExternal.forcedFreshEvent line 46
  6. theorem OAI.Balanced.CandidateMixedExternal.mixedExternalEvent_forces line 53
  7. theorem OAI.Balanced.CandidateMixedExternal.forcedFreshEvent_probability line 65
  8. theorem OAI.Balanced.CandidateMixedExternal.mixedExternalEvent_probability_le line 85
  9. def OAI.Balanced.CandidateMixedExternal.freshWitnessDirections line 117
  10. def OAI.Balanced.CandidateMixedExternal.oldWitnessDirections line 121
  11. theorem OAI.Balanced.CandidateMixedExternal.sum_freshWitness_probability_le line 125
  12. def OAI.Balanced.CandidateMixedExternal.mixedExternalProbabilitySum line 168
  13. theorem OAI.Balanced.CandidateMixedExternal.mixedExternalProbabilitySum_le_overlap line 176
  14. theorem OAI.Balanced.CandidateMixedExternal.mixedExternalProbabilitySum_le line 205