OAI/Geometry/RCD/Sobolev/HessianActionChain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Hessian chain rule in a gradient direction

The second scalar derivative cancels in the three-term action. Only the two existing bounded mixed Gram representatives are needed.

  1. theorem OAI.RegularPointCoordinates.localHessianAction_comp_direction line 19
  2. theorem OAI.RegularPointCoordinates.exists_local_hessian_log_direction line 56