OAI/Analysis/LipschitzEquivalence/FiniteApproximants.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.HilbertSlots.approxSlots_derivative_budget line 17
  2. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_derivative_close line 28
  3. def OAI.LipschitzCounterexample.HilbertSlots.finiteBlocks line 51
  4. instance OAI.LipschitzCounterexample.HilbertSlots.finiteBlocks_finiteDimensional line 54
  5. theorem OAI.LipschitzCounterexample.HilbertSlots.single_mem_finiteBlocks line 59
  6. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_bijective line 65
  7. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_bounds line 101
  8. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_head line 127
  9. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_prefix line 141
  10. theorem OAI.LipschitzCounterexample.HilbertSlots.approximant_tendsto line 147
  11. theorem OAI.LipschitzCounterexample.HilbertSlots.movingSlotsMap_bounds line 192
  12. theorem OAI.LipschitzCounterexample.HilbertSlots.movingSlotsMap_bijective line 203