OAI/Analysis/C0Absorption/Completion.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.C0Absorption.seminorm_lipschitz line 17
  2. theorem OAI.C0Absorption.completion_lipschitz line 24
  3. def OAI.C0Absorption.completedSeminorm line 35
  4. theorem OAI.C0Absorption.completedSeminorm_coe line 62
  5. theorem OAI.C0Absorption.completedSeminorm_continuous line 66
  6. theorem OAI.C0Absorption.completedSeminorm_le line 70
  7. def OAI.C0Absorption.PreSpace line 84
  8. instance OAI.C0Absorption.(instance at line 86) line 86
  9. instance OAI.C0Absorption.(instance at line 88) line 88
  10. instance OAI.C0Absorption.(instance at line 94) line 94
  11. def OAI.C0Absorption.TestSpace line 97
  12. instance OAI.C0Absorption.(instance at line 99) line 99
  13. instance OAI.C0Absorption.(instance at line 101) line 101
  14. instance OAI.C0Absorption.(instance at line 103) line 103
  15. def OAI.C0Absorption.toTestSpace line 106
  16. theorem OAI.C0Absorption.norm_toTestSpace line 109
  17. def OAI.C0Absorption.initialCoordinates line 112
  18. theorem OAI.C0Absorption.initialCoordinates_lipschitz line 115
  19. def OAI.C0Absorption.normCoordinates line 121
  20. theorem OAI.C0Absorption.normCoordinates_continuous line 124
  21. theorem OAI.C0Absorption.normCoordinates_coe line 127
  22. theorem OAI.C0Absorption.normCoordinates_norm line 131
  23. theorem OAI.C0Absorption.selectedCoordinate_le_norm line 139
  24. def OAI.C0Absorption.completedCoordinate line 145
  25. theorem OAI.C0Absorption.completedCoordinate_continuous line 149
  26. theorem OAI.C0Absorption.completedCoordinate_coe line 152
  27. theorem OAI.C0Absorption.normCoordinates_apply line 156
  28. theorem OAI.C0Absorption.completedCoordinate_summable line 169
  29. theorem OAI.C0Absorption.completedNorm_sq line 175
  30. def OAI.C0Absorption.prePoint line 182
  31. theorem OAI.C0Absorption.prePoint_lipschitz line 184
  32. theorem OAI.C0Absorption.prePoint_span line 192
  33. instance OAI.C0Absorption.(instance at line 202) line 202
  34. instance OAI.C0Absorption.(instance at line 207) line 207
  35. def OAI.C0Absorption.zeta line 210
  36. theorem OAI.C0Absorption.zeta_base line 212
  37. theorem OAI.C0Absorption.zeta_lipschitz line 216