OAI/Analysis/Cotype/WeightedCompact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Cotype.LevelSum line 15
  2. def OAI.Cotype.levelTerm line 17
  3. theorem OAI.Cotype.levelTerm_apply line 21
  4. theorem OAI.Cotype.levelTerm_norm line 25
  5. theorem OAI.Cotype.levelTerm_summable_norm line 33
  6. theorem OAI.Cotype.levelTerm_summable line 37
  7. def OAI.Cotype.weightedMap line 39
  8. theorem OAI.Cotype.weightedMap_norm line 42
  9. theorem OAI.Cotype.weightedMap_summable_apply line 49
  10. theorem OAI.Cotype.weightedMap_apply line 53
  11. theorem OAI.Cotype.levelTerm_compact line 58
  12. theorem OAI.Cotype.weightedMap_compact line 64
  13. theorem OAI.Cotype.weightedMap_single_zero line 71