OAI/Geometry/Riemannian/HarmonicCore/Sobolev.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.dirichletTests line 11
  2. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest line 23
  3. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.Derivative3 line 24
  4. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.ValueL2 line 25
  5. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.DerivativeL2 line 26
  6. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.SobolevPair line 27
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.value_memLp line 29
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_continuous line 33
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_compact line 38
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_norm_fderiv line 42
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.derivative_memLp line 46
  12. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.value line 51
  13. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.derivative line 54
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.poincare line 57
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_add_smooth line 76
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_smul_smooth line 82
  17. def OAI.HarmonicCounterexample.Main.SmoothMetric3.testValueLinear line 88
  18. def OAI.HarmonicCounterexample.Main.SmoothMetric3.testDerivativeLinear line 93
  19. def OAI.HarmonicCounterexample.Main.SmoothMetric3.testGraph line 108
  20. def OAI.HarmonicCounterexample.Main.SmoothMetric3.zeroSobolevSpace line 112
  21. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.ZeroSobolev line 115
  22. instance OAI.HarmonicCounterexample.Main.SmoothMetric3.zeroSobolev_complete line 117
  23. def OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevValue line 120
  24. def OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevDerivative line 123
  25. def OAI.HarmonicCounterexample.Main.SmoothMetric3.poincareConstant line 126
  26. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.poincareConstant_nonneg line 129
  27. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_poincare line 131
  28. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_norm_sq_le line 141