OAI/Analysis/C0Absorption/Norm.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.triple line 15
  2. theorem OAI.C0Absorption.triple_surjective line 18
  3. def OAI.C0Absorption.listConstant line 22
  4. theorem OAI.C0Absorption.listConstant_pos line 24
  5. def OAI.C0Absorption.listExponent line 28
  6. instance OAI.C0Absorption.(instance at line 30) line 30
  7. theorem OAI.C0Absorption.listExponent_ne_top line 32
  8. theorem OAI.C0Absorption.listExponent_toReal line 35
  9. def OAI.C0Absorption.alpha line 39
  10. theorem OAI.C0Absorption.alpha_pos line 41
  11. def OAI.C0Absorption.squareWeight line 46
  12. theorem OAI.C0Absorption.squareWeight_sq line 49
  13. theorem OAI.C0Absorption.squareWeight_pos line 54
  14. def OAI.C0Absorption.selectedCoordinate line 60
  15. theorem OAI.C0Absorption.selectedCoordinate_apply line 63
  16. theorem OAI.C0Absorption.weighted_bound line 67
  17. theorem OAI.C0Absorption.selectedCoordinate_bound line 77
  18. theorem OAI.C0Absorption.geometric_summable line 83
  19. theorem OAI.C0Absorption.geometric_tsum line 88
  20. theorem OAI.C0Absorption.selectedCoordinate_summable line 93
  21. def OAI.C0Absorption.selectedNorm line 106
  22. theorem OAI.C0Absorption.selectedNorm_sq line 109
  23. theorem OAI.C0Absorption.selectedNorm_molecule_le line 117