OAI/Analysis/LipschitzEquivalence/SeparatingCoordinates.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.SeparatingStages.psi line 12
  2. theorem OAI.LipschitzCounterexample.SeparatingStages.psi_nonneg line 14
  3. theorem OAI.LipschitzCounterexample.SeparatingStages.psi_pos_iff line 16
  4. theorem OAI.LipschitzCounterexample.SeparatingStages.psi_ne_zero_iff line 31
  5. theorem OAI.LipschitzCounterexample.SeparatingStages.psi_contDiff line 37
  6. abbrev OAI.LipschitzCounterexample.SeparatingStages.Label line 40
  7. abbrev OAI.LipschitzCounterexample.SeparatingStages.Stage line 41
  8. abbrev OAI.LipschitzCounterexample.SeparatingStages.CubeSpace line 42
  9. def OAI.LipschitzCounterexample.SeparatingStages.G line 44
  10. theorem OAI.LipschitzCounterexample.SeparatingStages.G_apply line 47
  11. theorem OAI.LipschitzCounterexample.SeparatingStages.rounding_label line 50
  12. theorem OAI.LipschitzCounterexample.SeparatingStages.G_ne_zero line 72
  13. def OAI.LipschitzCounterexample.SeparatingStages.normalized line 84
  14. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_normalized line 86
  15. theorem OAI.LipschitzCounterexample.SeparatingStages.normalized_support line 91
  16. theorem OAI.LipschitzCounterexample.SeparatingStages.support_disjoint line 101
  17. def OAI.LipschitzCounterexample.SeparatingStages.cube line 117
  18. theorem OAI.LipschitzCounterexample.SeparatingStages.cube_compact line 119
  19. theorem OAI.LipschitzCounterexample.SeparatingStages.G_contDiff line 130
  20. theorem OAI.LipschitzCounterexample.SeparatingStages.normalized_contDiffAt line 138
  21. theorem OAI.LipschitzCounterexample.SeparatingStages.normalized_derivative_bound line 143
  22. abbrev OAI.LipschitzCounterexample.SeparatingStages.BlockLabel line 156
  23. abbrev OAI.LipschitzCounterexample.SeparatingStages.Block line 157
  24. abbrev OAI.LipschitzCounterexample.SeparatingStages.U line 158
  25. abbrev OAI.LipschitzCounterexample.SeparatingStages.V line 159
  26. abbrev OAI.LipschitzCounterexample.SeparatingStages.M line 160
  27. abbrev OAI.LipschitzCounterexample.SeparatingStages.ScalarIndex line 161
  28. def OAI.LipschitzCounterexample.SeparatingStages.enumerate line 163
  29. def OAI.LipschitzCounterexample.SeparatingStages.scalarCoordinate line 165
  30. theorem OAI.LipschitzCounterexample.SeparatingStages.scalarCoordinate_norm line 171
  31. theorem OAI.LipschitzCounterexample.SeparatingStages.scalarCoordinate_separate line 179
  32. theorem OAI.LipschitzCounterexample.SeparatingStages.tanh_contDiff line 191
  33. theorem OAI.LipschitzCounterexample.SeparatingStages.tanh_hasDerivAt line 196
  34. theorem OAI.LipschitzCounterexample.SeparatingStages.tanh_deriv_norm line 204
  35. def OAI.LipschitzCounterexample.SeparatingStages.p line 209
  36. theorem OAI.LipschitzCounterexample.SeparatingStages.p_mem line 211
  37. theorem OAI.LipschitzCounterexample.SeparatingStages.p_contDiff line 214
  38. theorem OAI.LipschitzCounterexample.SeparatingStages.p_separate line 217
  39. theorem OAI.LipschitzCounterexample.SeparatingStages.p_fderiv_bound line 223
  40. theorem OAI.LipschitzCounterexample.SeparatingStages.p_lipschitz line 238
  41. def OAI.LipschitzCounterexample.SeparatingStages.pVector line 242
  42. theorem OAI.LipschitzCounterexample.SeparatingStages.pVector_mem line 244
  43. theorem OAI.LipschitzCounterexample.SeparatingStages.pVector_contDiff line 246
  44. def OAI.LipschitzCounterexample.SeparatingStages.pVectorBound line 249
  45. theorem OAI.LipschitzCounterexample.SeparatingStages.pVector_lipschitz line 251
  46. def OAI.LipschitzCounterexample.SeparatingStages.coordEmbed line 263
  47. theorem OAI.LipschitzCounterexample.SeparatingStages.coordEmbed_apply line 275
  48. theorem OAI.LipschitzCounterexample.SeparatingStages.coordEmbed_on line 284
  49. theorem OAI.LipschitzCounterexample.SeparatingStages.coordEmbed_off line 292
  50. def OAI.LipschitzCounterexample.SeparatingStages.stageEmbedding line 307
  51. def OAI.LipschitzCounterexample.SeparatingStages.Wzero line 311
  52. def OAI.LipschitzCounterexample.SeparatingStages.W line 313
  53. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_Wzero line 316
  54. theorem OAI.LipschitzCounterexample.SeparatingStages.norm_W line 318
  55. theorem OAI.LipschitzCounterexample.SeparatingStages.W_contDiff line 322
  56. def OAI.LipschitzCounterexample.SeparatingStages.stageBound line 329
  57. theorem OAI.LipschitzCounterexample.SeparatingStages.stageBound_nonneg line 331
  58. theorem OAI.LipschitzCounterexample.SeparatingStages.W_fderiv_bound line 334
  59. theorem OAI.LipschitzCounterexample.SeparatingStages.W_on line 353
  60. theorem OAI.LipschitzCounterexample.SeparatingStages.W_off line 357
  61. theorem OAI.LipschitzCounterexample.SeparatingStages.W_at_zero line 361
  62. theorem OAI.LipschitzCounterexample.SeparatingStages.W_at_other line 366
  63. theorem OAI.LipschitzCounterexample.SeparatingStages.inner_coordEmbed_zero line 372
  64. theorem OAI.LipschitzCounterexample.SeparatingStages.inner_Wzero_W line 382
  65. theorem OAI.LipschitzCounterexample.SeparatingStages.inner_W_W line 386