OAI/Geometry/RCD/Harmonic/EuclideanHarmonicSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the Laplacian of a squared harmonic function

  1. theorem OAI.RegularPointCoordinates.laplacian_square_formula line 13
  2. theorem OAI.RegularPointCoordinates.harmonic_square_laplacian_nonneg line 37