OAI/Geometry/Riemannian/HarmonicCore/MaximumPrinciple.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.second_deriv_nonpos_at_localMax line 16
  2. lemma OAI.HarmonicCounterexample.Main.hessian_nonpos_at_localMax line 53
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordinate_expansion line 73
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.hessian_coordinates line 77
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_nonpos_at_localMax line 91
  6. def OAI.HarmonicCounterexample.Main.SmoothMetric3.coordinateBarrier line 131
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordinateBarrier_smooth line 133
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.fderiv_coordinateBarrier line 138
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_coordinateBarrier line 145
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.exists_positive_barrier line 164
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.strict_maximum_principle_closedBall line 190
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.maximum_principle_closedBall line 206
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonic_comparison_closedBall line 243
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonic_unique_closedBall line 268
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonic_positive_closedBall line 284
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonic_constant_closedBall line 293