OAI/Combinatorics/BalancedRyser/Profiles/ProfileEmpiricalMeasure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.finiteDirac line 13
  2. theorem OAI.Balanced.scaled_dirac_sum_mass line 16
  3. theorem OAI.Balanced.empiricalProfileMeasure_mass line 35
  4. theorem OAI.Balanced.isBoundedProfile_iff_mem_profiles line 45
  5. abbrev OAI.Balanced.BoundedProfile line 50
  6. def OAI.Balanced.boundedLineProfile line 52
  7. def OAI.Balanced.boundedEmpiricalProfileMeasure line 58
  8. theorem OAI.Balanced.boundedEmpiricalProfileMeasure_mass line 66
  9. theorem OAI.Balanced.finiteDirac_map line 78
  10. theorem OAI.Balanced.scaled_dirac_sum_map line 85
  11. theorem OAI.Balanced.boundedEmpiricalProfileMeasure_map line 96
  12. def OAI.Balanced.boundedPlaneProfile line 104
  13. theorem OAI.Balanced.profile_witness_ratio_mem_Icc line 112
  14. theorem OAI.Balanced.boundedEmpiricalProfileMeasure_deletion_mass_le line 119
  15. theorem OAI.Balanced.exists_actual_profile_subsequence line 131