OAI/Combinatorics/BalancedRyser/Incidence/ProfileEmpiricalIncidence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.FiniteProfile.lineProfile_mem_Icc line 16
  2. theorem OAI.Balanced.FiniteProfile.planeProfile_mem_Icc line 27
  3. theorem OAI.Balanced.FiniteProfile.coe_empiricalProfileMeasure line 40
  4. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_integral line 52
  5. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_mass line 59
  6. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_deletion_incidence line 65
  7. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_cover_incidence line 72
  8. theorem OAI.Balanced.FiniteProfile.ae_empiricalProfileMeasure_of_forall line 79
  9. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_unit_coordinates line 88
  10. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_deletion_zero_row line 95
  11. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_cover_zero_column line 105
  12. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_deletion_mass line 115
  13. theorem OAI.Balanced.FiniteProfile.empiricalProfileMeasure_deletion_mass_tendsto line 124