OAI/Combinatorics/BalancedRyser/Candidates/ExternalFreshGeneratorBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ExternalAssembly.witness_probability_le_lines line 18
  2. theorem OAI.Balanced.ExternalAssembly.witness_probability_eq_zero_of_first_target line 32
  3. theorem OAI.Balanced.ExternalAssembly.witness_probability_eq_zero_of_second_generator line 44
  4. theorem OAI.Balanced.ExternalAssembly.old_key_probability_le line 56
  5. theorem OAI.Balanced.ExternalAssembly.old_fresh_key_probability_le line 78
  6. def OAI.Balanced.ExternalAssembly.freshGeneratorLabels line 102
  7. theorem OAI.Balanced.ExternalAssembly.filter_freshGeneratorLabels line 105
  8. theorem OAI.Balanced.ExternalAssembly.freshGenerators_oldOld_integral_le line 116
  9. theorem OAI.Balanced.ExternalAssembly.freshGenerators_oldFresh_integral_le line 146
  10. theorem OAI.Balanced.ExternalAssembly.freshGenerators_firstOld_integral_le line 188