OAI/Analysis/C0Absorption/Coordinates.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.C0Absorption.C0Ball line 11
  2. abbrev OAI.C0Absorption.Cube line 13
  3. theorem OAI.C0Absorption.c0_norm_apply_le line 15
  4. theorem OAI.C0Absorption.c0_norm_le line 18
  5. def OAI.C0Absorption.c0Eval line 21
  6. theorem OAI.C0Absorption.c0Eval_apply line 27
  7. def OAI.C0Absorption.cubeRestrict line 29
  8. def OAI.C0Absorption.finsuppToC0 line 37
  9. theorem OAI.C0Absorption.finsuppToC0_apply line 43
  10. def OAI.C0Absorption.atom line 45
  11. theorem OAI.C0Absorption.atom_apply line 47
  12. theorem OAI.C0Absorption.atom_norm line 50
  13. def OAI.C0Absorption.truncate line 58
  14. theorem OAI.C0Absorption.truncate_apply line 60
  15. theorem OAI.C0Absorption.c0_tendsto_zero line 76
  16. theorem OAI.C0Absorption.truncate_tendsto line 79
  17. theorem OAI.C0Absorption.truncate_mem_span line 97
  18. theorem OAI.C0Absorption.c0_span_dense line 103
  19. instance OAI.C0Absorption.c0_separable line 108
  20. def OAI.C0Absorption.extendFinite line 114
  21. theorem OAI.C0Absorption.extendFinite_apply line 119
  22. theorem OAI.C0Absorption.extendFinite_norm_le line 124
  23. def OAI.C0Absorption.cubeExtend line 134
  24. theorem OAI.C0Absorption.cubeRestrict_extend line 141
  25. theorem OAI.C0Absorption.cubeRestrict_lipschitz line 148
  26. theorem OAI.C0Absorption.cubeExtend_lipschitz line 157
  27. theorem OAI.C0Absorption.cubeExtend_isometry line 170
  28. abbrev OAI.C0Absorption.GridIndex line 177
  29. def OAI.C0Absorption.gridPoint line 179
  30. def OAI.C0Absorption.nearestGridIndex line 188
  31. theorem OAI.C0Absorption.nearestGrid_dist line 203
  32. def OAI.C0Absorption.dyadic line 214
  33. theorem OAI.C0Absorption.dyadic_pos line 216
  34. theorem OAI.C0Absorption.dyadic_tendsto line 218
  35. abbrev OAI.C0Absorption.OperationGrid line 223
  36. def OAI.C0Absorption.operationGridPoint line 225
  37. def OAI.C0Absorption.nearestOperationGrid line 228
  38. theorem OAI.C0Absorption.operationGrid_mesh line 231
  39. theorem OAI.C0Absorption.nearestOperationGrid_dist line 234
  40. def OAI.C0Absorption.coordinateTail line 246
  41. theorem OAI.C0Absorption.coordinateTail_apply line 248
  42. def OAI.C0Absorption.tau line 253
  43. theorem OAI.C0Absorption.tau_nonneg line 255
  44. theorem OAI.C0Absorption.coordinateTail_sub line 257
  45. theorem OAI.C0Absorption.tau_le_norm line 263
  46. theorem OAI.C0Absorption.tau_lipschitz line 271
  47. theorem OAI.C0Absorption.tau_antitone line 281
  48. theorem OAI.C0Absorption.tau_tendsto_zero line 291
  49. def OAI.C0Absorption.tailFactor line 296
  50. theorem OAI.C0Absorption.tailFactor_nonneg line 298
  51. theorem OAI.C0Absorption.tailFactor_le_one line 301
  52. theorem OAI.C0Absorption.tailFactor_eq_one line 303
  53. theorem OAI.C0Absorption.tailFactor_eq_zero line 310
  54. theorem OAI.C0Absorption.tailFactor_lipschitz line 315
  55. theorem OAI.C0Absorption.tailFactor_tendsto_one line 334
  56. theorem OAI.C0Absorption.tailFactor_support line 342
  57. theorem OAI.C0Absorption.remainderTail_support line 350