`OAI/Geometry/RCD/Sobolev/CanonicalHessianConstantShift.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local constant shifts preserve the canonical Hessian direction

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonical_hessian_locality_of_constant line 17