OAI/Combinatorics/BalancedRyser/Probability/MultiplicityLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.tsum_abs_sub_distance_le line 16
  2. theorem OAI.Balanced.tendsto_totalVariation_to_fixed line 38
  3. theorem OAI.Balanced.deletionPoissonMass_hasSum line 56
  4. theorem OAI.Balanced.empiricalMultiplicityMass_nonneg line 61
  5. theorem OAI.Balanced.deletionMultiplicityTV_tendsto line 67
  6. theorem OAI.Balanced.planeProfile_empty_cover_zero line 79
  7. theorem OAI.Balanced.multiplicityFailureClass_limit_density_zero line 86
  8. theorem OAI.Balanced.multiplicityFailureClass_limit_coordinates line 97
  9. theorem OAI.Balanced.empiricalMultiplicityMass_firstMoment_hasSum line 108
  10. theorem OAI.Balanced.empiricalMultiplicityMass_mean_le line 127
  11. theorem OAI.Balanced.multiplicityFailureClass_limit_probability line 139
  12. theorem OAI.Balanced.multiplicityFailureClass_limit_tv line 161