OAI/Analysis/LipschitzEquivalence/Localization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.LocalizedLinearization.lipschitz_sub_const line 16
  2. theorem OAI.LipschitzCounterexample.LocalizedLinearization.lipschitz_const_sub line 24
  3. def OAI.LipschitzCounterexample.LocalizedLinearization.normalized line 31
  4. def OAI.LipschitzCounterexample.LocalizedLinearization.test line 37
  5. theorem OAI.LipschitzCounterexample.LocalizedLinearization.test_point line 46
  6. theorem OAI.LipschitzCounterexample.LocalizedLinearization.norm_test_apply_le line 49
  7. theorem OAI.LipschitzCounterexample.LocalizedLinearization.norm_normalized_le line 54
  8. def OAI.LipschitzCounterexample.LocalizedLinearization.cutoff line 60
  9. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_nonneg line 64
  10. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_le_one line 66
  11. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_zero line 70
  12. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_one line 80
  13. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_lipschitz line 93
  14. theorem OAI.LipschitzCounterexample.LocalizedLinearization.product_lipschitz line 110
  15. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_product_lipschitz line 146
  16. theorem OAI.LipschitzCounterexample.LocalizedLinearization.annular_product_lipschitz line 158
  17. def OAI.LipschitzCounterexample.LocalizedLinearization.DisjointTests line 170
  18. theorem OAI.LipschitzCounterexample.LocalizedLinearization.DisjointTests.exists_index line 174
  19. def OAI.LipschitzCounterexample.LocalizedLinearization.activeIndex line 183
  20. theorem OAI.LipschitzCounterexample.LocalizedLinearization.activeIndex_spec line 187
  21. def OAI.LipschitzCounterexample.LocalizedLinearization.disjointMap line 190
  22. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjointMap_apply line 194
  23. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjointMap_lipschitz line 203
  24. def OAI.LipschitzCounterexample.LocalizedLinearization.disjointOperator line 235
  25. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjointOperator_point line 239
  26. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjointOperator_coord line 245
  27. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjoint_tests_vanish line 261
  28. theorem OAI.LipschitzCounterexample.LocalizedLinearization.finite_avoid_radius line 271
  29. theorem OAI.LipschitzCounterexample.LocalizedLinearization.test_combination_zero line 291
  30. theorem OAI.LipschitzCounterexample.LocalizedLinearization.test_normalized_sub line 300
  31. theorem OAI.LipschitzCounterexample.LocalizedLinearization.exists_small_cutoff line 314
  32. theorem OAI.LipschitzCounterexample.LocalizedLinearization.shrinking_tests line 359