OAI/Geometry/RCD/Sobolev/EuclideanHarmonicHessianConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean harmonic Hessian input from radial averaging

  1. theorem OAI.RegularPointCoordinates.euclideanHarmonicHessianInput line 17

    Source documentation

    The exact interior Hessian estimate for normalized harmonic models. The radius and the function are chosen after the dimensional constant.

    theorem euclideanHarmonicHessianInput {n : ℕ} (hn : 0 < n) : EuclideanHarmonicHessianInput n := by
…

    Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput