OAI/Geometry/RCD/Sobolev/SobolevSecondVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact Hessian cancellation in a twice differentiated heat product

The identity uses only weak Laplacians, bounded Sobolev product rules, and three actual Sobolev Gram representatives. All terms are in L2.

  1. theorem OAI.RegularPointCoordinates.sobolev_second_variation_hessian line 19