OAI/Combinatorics/BalancedRyser/Profiles/ProfileWitnessPayment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileWitnessPayment.projection_mass_le line 17
  2. theorem OAI.Balanced.ProfileWitnessPayment.projection_probability_le line 28
  3. def OAI.Balanced.ProfileWitnessPayment.witnesses line 50
  4. theorem OAI.Balanced.ProfileWitnessPayment.mem_witnesses line 53
  5. theorem OAI.Balanced.ProfileWitnessPayment.card_witnesses line 57
  6. theorem OAI.Balanced.ProfileWitnessPayment.card_witnesses_pos line 62
  7. def OAI.Balanced.ProfileWitnessPayment.pairMarkAverage line 68
  8. theorem OAI.Balanced.ProfileWitnessPayment.fixed_size_payment line 73
  9. theorem OAI.Balanced.ProfileWitnessPayment.witness_probability_le_sum_fixed_sizes line 88
  10. theorem OAI.Balanced.ProfileWitnessPayment.all_sizes_payment line 116
  11. theorem OAI.Balanced.ProfileWitnessPayment.cancellation_payment line 132
  12. theorem OAI.Balanced.ProfileWitnessPayment.eventually_superexponential_payment line 150
  13. theorem OAI.Balanced.ProfileWitnessPayment.counting_of_mark_bounds line 173