OAI/Geometry/Riemannian/HarmonicCore/BoundaryBarrier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.christoffel_contDiff line 18
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_add_at line 29
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_smul_at line 45
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_const line 66
  5. def OAI.HarmonicCounterexample.Main.SmoothMetric3.planeExponential line 70
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.planeExponential_smooth line 72
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.fderiv_planeExponential line 75
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_coordinateVector line 80
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_planeExponential line 83
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.exists_positive_planeExponential line 101
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.supporting_plane_strict line 138
  12. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.exists_boundary_barrier line 147