OAI/Geometry/RCD/Heat/HeatBridgePairingDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating bounded tests of the forward/backward heat product

The derivative is taken in L² before pairing. No exchange of a pointwise derivative with an improper spatial integral is needed.

  1. theorem OAI.RegularPointCoordinates.kernelHeat_weighted_pairing line 19
  2. theorem OAI.RegularPointCoordinates.kernelHeat_bridge_pairing_hasDerivAt line 30