OAI/Analysis/LipschitzEquivalence/SupportedDuality.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.FreeSpace.exists_finite_approx line 20
  2. theorem OAI.LipschitzCounterexample.FreeSpace.combination_mem_supported line 25
  3. theorem OAI.LipschitzCounterexample.FreeSpace.dual_point_lipschitz line 30
  4. theorem OAI.LipschitzCounterexample.FreeSpace.dual_as_test line 34
  5. theorem OAI.LipschitzCounterexample.FreeSpace.exists_vanishing_test line 43
  6. theorem OAI.LipschitzCounterexample.LocalizedLinearization.lipschitz_effective_smul line 92
  7. def OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff line 122
  8. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_lipschitz line 125
  9. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_nonneg line 133
  10. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_le_one line 136
  11. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_one line 139
  12. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_zero line 144
  13. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_nonzero line 149
  14. theorem OAI.LipschitzCounterexample.LocalizedLinearization.setCutoff_support_bounded line 156