OAI/Geometry/RCD/Sobolev/EuclideanConstantEnergyRigidity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local rigidity of harmonic functions with constant gradient norm

  1. theorem OAI.RegularPointCoordinates.laplacian_finite_sum line 12
  2. theorem OAI.RegularPointCoordinates.harmonic_constant_energy_second_directional_zero line 26
  3. theorem OAI.RegularPointCoordinates.harmonic_constant_energy_hessian_zero line 67
  4. theorem OAI.RegularPointCoordinates.harmonic_constant_energy_affine line 88