OAI/Combinatorics/Chromatic/GradedAlgebra/EnergyLimit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.EnergyLaurent.finite_above line 15
  2. def OAI.ElementaryPositivity.EnergyLaurent.finiteSupportCutoff line 29
  3. lemma OAI.ElementaryPositivity.EnergyLaurent.support_le_cutoff line 32
  4. def OAI.ElementaryPositivity.EnergyLaurent.supportRestrictedSeries line 37
  5. lemma OAI.ElementaryPositivity.EnergyLaurent.supportRestricted_coeff line 41
  6. lemma OAI.ElementaryPositivity.EnergyLaurent.supportRestricted_agrees line 53
  7. theorem OAI.ElementaryPositivity.EnergyLaurent.finiteSupport_converges line 61
  8. def OAI.ElementaryPositivity.UnitSelections.startSupport line 80
  9. def OAI.ElementaryPositivity.UnitSelections.startEmbedding line 83
  10. lemma OAI.ElementaryPositivity.UnitSelections.startSupport_iff line 86
  11. def OAI.ElementaryPositivity.UnitSelections.finiteStartEquiv line 99
  12. lemma OAI.ElementaryPositivity.UnitSelections.finiteStart_energy line 105
  13. lemma OAI.ElementaryPositivity.UnitSelections.finiteStart_admissible line 113
  14. def OAI.ElementaryPositivity.UnitSelections.finiteStartSeries line 119
  15. lemma OAI.ElementaryPositivity.UnitSelections.finiteStartSeries_eq line 123
  16. theorem OAI.ElementaryPositivity.UnitSelections.finiteStartSeries_converges line 128
  17. lemma OAI.ElementaryPositivity.UnitSelections.stringSeries_congr line 144
  18. lemma OAI.ElementaryPositivity.UnitSelections.stringSeries_reindex line 153
  19. lemma OAI.ElementaryPositivity.UnitSelections.stringEmbedding_admissible line 159
  20. lemma OAI.ElementaryPositivity.UnitSelections.stringSeries_zero line 168
  21. lemma OAI.ElementaryPositivity.UnitSelections.stringSeries_empty line 185