OAI/Combinatorics/BalancedRyser/Profiles/ProfileMarginalTV.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileMarginalTV.tsum_abs_marginal_sub_le line 13
  2. theorem OAI.Balanced.ProfileMarginalTV.totalVariation_marginal_le line 27
  3. theorem OAI.Balanced.ProfileMarginalTV.tendsto_marginal_totalVariation line 33
  4. theorem OAI.Balanced.ProfileMarginalTV.abs_tsum_abs_sub_sub_le line 44
  5. theorem OAI.Balanced.ProfileMarginalTV.tendsto_totalVariation_distance line 60
  6. theorem OAI.Balanced.ProfileMarginalTV.deletionPoissonMass_hasSum line 72
  7. theorem OAI.Balanced.ProfileMarginalTV.lineMultiplicity_eq_deletionMultiplicity line 83
  8. theorem OAI.Balanced.ProfileMarginalTV.planeProfile_row_hasSum line 86
  9. theorem OAI.Balanced.ProfileMarginalTV.tsum_planeProfile_row line 99
  10. theorem OAI.Balanced.ProfileMarginalTV.empiricalMultiplicity_tendsto_marginal line 110
  11. theorem OAI.Balanced.ProfileMarginalTV.deletionMultiplicityTV_tendsto_zero line 124
  12. theorem OAI.Balanced.ProfileMarginalTV.not_poisson_marginal_of_bad_tv line 134
  13. theorem OAI.Balanced.ProfileMarginalTV.deletionMultiplicityTV_tendsto line 146
  14. theorem OAI.Balanced.ProfileMarginalTV.bad_tv_persists line 158
  15. theorem OAI.Balanced.ProfileMarginalTV.poisson_marginal_of_vanishing_tolerance line 168