OAI/Geometry/Riemannian/HarmonicCore/WeakMaximum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smoothTransition_deriv_bound line 16
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_maximum_from_transition line 36
  3. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.affine_weak_maximum line 87
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.negative_sphere_collar line 106
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.strict_boundary_test_extension line 140