OAI/Combinatorics/IndependentSets/Encoding/Normalizer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.Coefficient.normalizer line 8
  2. def OAI.LargeIndependentSets.Coefficient.levelMass line 9
  3. def OAI.LargeIndependentSets.Coefficient.mass line 11
  4. lemma OAI.LargeIndependentSets.Coefficient.normalizer_pos line 14
  5. lemma OAI.LargeIndependentSets.Coefficient.levelMass_pos line 20
  6. lemma OAI.LargeIndependentSets.Coefficient.levelMass_nonneg line 23
  7. lemma OAI.LargeIndependentSets.Coefficient.levelMass_total line 26
  8. lemma OAI.LargeIndependentSets.Coefficient.mass_nonneg line 31
  9. lemma OAI.LargeIndependentSets.Coefficient.mass_total line 35
  10. def OAI.LargeIndependentSets.Coefficient.lower line 41
  11. lemma OAI.LargeIndependentSets.Coefficient.lower_injective_on_positive line 45
  12. lemma OAI.LargeIndependentSets.Coefficient.levelMass_lower line 56
  13. lemma OAI.LargeIndependentSets.Coefficient.mass_lower line 64
  14. theorem OAI.LargeIndependentSets.Coefficient.one_level_event_bound line 78
  15. theorem OAI.LargeIndependentSets.Coefficient.positive_coefficient_bound line 104