OAI/Geometry/Riemannian/HarmonicCore/Translation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2 line 12
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2_coe line 16
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2_norm line 21
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_translate line 25
  5. def OAI.HarmonicCounterexample.Main.SmoothMetric3.translatePair line 32
  6. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.translate line 37
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translatePair_test line 50
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translatePair_mem line 73
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.translateSobolev line 83
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_compact_derivative_lipschitz line 86
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_compact_taylor_bound line 94
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2_zero line 106
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2_add line 112
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.translateL2_inner line 121
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_taylor_error_vanishes line 135
  16. def OAI.HarmonicCounterexample.Main.SmoothMetric3.testDirection line 158
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_taylor_error_coe line 161
  18. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_translation_taylor line 176
  19. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_translation_hasDerivAt_zero line 206
  20. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_translation_hasDerivAt line 227
  21. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.testDirection_norm_le line 240
  22. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_translation_bound line 249
  23. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_translation_bound line 258