OAI/Analysis/LipschitzEquivalence/HilbertBijection.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.SeparatingStages.stage line 13
  2. def OAI.LipschitzCounterexample.SeparatingStages.bounds line 17
  3. theorem OAI.LipschitzCounterexample.SeparatingStages.bounds_nonneg line 21
  4. theorem OAI.LipschitzCounterexample.SeparatingStages.stage_contDiff line 26
  5. theorem OAI.LipschitzCounterexample.SeparatingStages.stage_fderiv_bound line 31
  6. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_stage line 40
  7. theorem OAI.LipschitzCounterexample.SeparatingStages.inner_stage line 45
  8. def OAI.LipschitzCounterexample.SeparatingStages.slot line 61
  9. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_slot line 64
  10. theorem OAI.LipschitzCounterexample.SeparatingStages.slot_contDiff line 68
  11. theorem OAI.LipschitzCounterexample.SeparatingStages.slot_derivative_budget line 75
  12. def OAI.LipschitzCounterexample.SeparatingStages.h line 88
  13. theorem OAI.LipschitzCounterexample.SeparatingStages.h_bounds line 91
  14. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_h line 95
  15. theorem OAI.LipschitzCounterexample.SeparatingStages.h_zero line 97
  16. theorem OAI.LipschitzCounterexample.SeparatingStages.h_lipschitz line 99
  17. theorem OAI.LipschitzCounterexample.SeparatingStages.h_symm_lipschitz line 102
  18. def OAI.LipschitzCounterexample.SeparatingStages.D line 110
  19. theorem OAI.LipschitzCounterexample.SeparatingStages.D_zero line 112
  20. theorem OAI.LipschitzCounterexample.SeparatingStages.fst_lipschitz line 114
  21. theorem OAI.LipschitzCounterexample.SeparatingStages.D_lipschitz line 119
  22. theorem OAI.LipschitzCounterexample.SeparatingStages.D_coord line 130
  23. instance OAI.LipschitzCounterexample.SeparatingStages.(instance at line 136) line 136
  24. def OAI.LipschitzCounterexample.SeparatingStages.q line 153
  25. theorem OAI.LipschitzCounterexample.SeparatingStages.q_point line 155
  26. theorem OAI.LipschitzCounterexample.SeparatingStages.q_norm line 158