OAI/Analysis/LipschitzEquivalence/HilbertDecomposition.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LipschitzCounterexample.HilbertSlots.HilbertSum line 16
  2. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_sq_tsum line 19
  3. theorem OAI.LipschitzCounterexample.HilbertSlots.summable_norm_sq line 23
  4. def OAI.LipschitzCounterexample.HilbertSlots.embed line 28
  5. theorem OAI.LipschitzCounterexample.HilbertSlots.embed_apply line 37
  6. def OAI.LipschitzCounterexample.HilbertSlots.coeff line 40
  7. theorem OAI.LipschitzCounterexample.HilbertSlots.coeff_apply line 53
  8. theorem OAI.LipschitzCounterexample.HilbertSlots.inner_slot_self line 57
  9. theorem OAI.LipschitzCounterexample.HilbertSlots.coeff_embed line 60
  10. def OAI.LipschitzCounterexample.HilbertSlots.perp line 65
  11. theorem OAI.LipschitzCounterexample.HilbertSlots.perp_apply line 68
  12. theorem OAI.LipschitzCounterexample.HilbertSlots.coeff_perp line 71
  13. theorem OAI.LipschitzCounterexample.HilbertSlots.perp_embed line 75
  14. theorem OAI.LipschitzCounterexample.HilbertSlots.perp_perp line 80
  15. theorem OAI.LipschitzCounterexample.HilbertSlots.perp_add_embed line 84
  16. theorem OAI.LipschitzCounterexample.HilbertSlots.inner_perp_embed line 89
  17. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_perp_add_embed_sq line 98
  18. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_perp_sq line 103
  19. def OAI.LipschitzCounterexample.HilbertSlots.interleaveRaw line 112
  20. theorem OAI.LipschitzCounterexample.HilbertSlots.interleaveRaw_even line 115
  21. theorem OAI.LipschitzCounterexample.HilbertSlots.interleaveRaw_odd line 120
  22. theorem OAI.LipschitzCounterexample.HilbertSlots.interleave_hasSum line 125
  23. def OAI.LipschitzCounterexample.HilbertSlots.interleaveSeq line 134
  24. def OAI.LipschitzCounterexample.HilbertSlots.interleave line 137
  25. theorem OAI.LipschitzCounterexample.HilbertSlots.interleave_even line 157
  26. theorem OAI.LipschitzCounterexample.HilbertSlots.interleave_odd line 159
  27. def OAI.LipschitzCounterexample.HilbertSlots.subsequence line 162
  28. theorem OAI.LipschitzCounterexample.HilbertSlots.subsequence_apply line 166
  29. def OAI.LipschitzCounterexample.HilbertSlots.split line 169
  30. theorem OAI.LipschitzCounterexample.HilbertSlots.interleave_split line 173
  31. theorem OAI.LipschitzCounterexample.HilbertSlots.split_interleave line 178
  32. def OAI.LipschitzCounterexample.HilbertSlots.interleaveEquiv line 184
  33. def OAI.LipschitzCounterexample.HilbertSlots.frozenCLM line 193
  34. def OAI.LipschitzCounterexample.HilbertSlots.frozen line 200
  35. def OAI.LipschitzCounterexample.HilbertSlots.frozenInv line 216
  36. theorem OAI.LipschitzCounterexample.HilbertSlots.frozen_right_inv line 220
  37. def OAI.LipschitzCounterexample.HilbertSlots.frozenEquiv line 228
  38. theorem OAI.LipschitzCounterexample.HilbertSlots.frozen_apply line 239
  39. theorem OAI.LipschitzCounterexample.HilbertSlots.frozenInv_fst line 247
  40. theorem OAI.LipschitzCounterexample.HilbertSlots.frozenInv_snd line 251
  41. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_frozenInv line 254
  42. theorem OAI.LipschitzCounterexample.HilbertSlots.frozenInv_fst_sq line 257
  43. theorem OAI.LipschitzCounterexample.HilbertSlots.sum_pairs line 267
  44. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_prefix_energy line 276
  45. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_tail_energy line 295
  46. def OAI.LipschitzCounterexample.HilbertSlots.moving line 311
  47. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_moving line 316
  48. theorem OAI.LipschitzCounterexample.HilbertSlots.moving_zero line 321