OAI/Geometry/RCD/Sobolev/CanonicalHessianApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every bounded regular gradient approximation has the canonical Hessian limit

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.hessian_limit_eq_canonical line 18