OAI/Geometry/RCD/Heat/HeatBridgeSecondDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact second variation of bounded heat-bridge pairings

All derivatives are taken in L2 before the bounded multiplier is paired. The coefficient contains the two actual iterated generators and the mixed first-generator term. No spatial regularity of the bounded test is assumed.

  1. def OAI.RegularPointCoordinates.heatBridgeVariation line 20
  2. def OAI.RegularPointCoordinates.heatBridgeSecondVariation line 24
  3. theorem OAI.RegularPointCoordinates.heatBridgeVariation_hasDerivAt line 29
  4. theorem OAI.RegularPointCoordinates.kernelHeat_bridge_pairing_hasDerivAt_variation line 56
  5. theorem OAI.RegularPointCoordinates.kernelHeat_bridge_pairing_second_hasDerivAt line 71