OAI/Analysis/LipschitzEquivalence/MovingSlots.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.HilbertSlots.scalarSlot line 14
  2. def OAI.LipschitzCounterexample.HilbertSlots.slotCoord line 17
  3. def OAI.LipschitzCounterexample.HilbertSlots.movingSlotsMap line 22
  4. theorem OAI.LipschitzCounterexample.HilbertSlots.movingSlotsMap_apply line 24
  5. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_movingSlotsMap line 28
  6. theorem OAI.LipschitzCounterexample.HilbertSlots.scalarSlot_contDiff line 31
  7. theorem OAI.LipschitzCounterexample.HilbertSlots.slotCoord_contDiff line 41
  8. def OAI.LipschitzCounterexample.HilbertSlots.approxSlots line 48
  9. theorem OAI.LipschitzCounterexample.HilbertSlots.approxSlots_norm line 52
  10. theorem OAI.LipschitzCounterexample.HilbertSlots.approxSlots_contDiff line 59
  11. def OAI.LipschitzCounterexample.HilbertSlots.approximant line 66
  12. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_tail line 69
  13. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_eq_sum line 87
  14. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_contDiff line 102
  15. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_fstCoord line 122
  16. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_sndCoord line 127
  17. theorem OAI.LipschitzCounterexample.HilbertSlots.differentiable_fstCoord line 133
  18. theorem OAI.LipschitzCounterexample.HilbertSlots.differentiable_sndCoord line 136
  19. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_scalarSlot_apply line 145
  20. theorem OAI.LipschitzCounterexample.HilbertSlots.differentiable_scalarSlot line 158
  21. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_slotCoord_apply line 166
  22. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_movingSlotsMap_apply line 182
  23. theorem OAI.LipschitzCounterexample.HilbertSlots.fderiv_movingSlotsMap_sub_frozen line 205
  24. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_fderiv_movingSlotsMap_sub_frozen line 232