OAI/Geometry/RCD/Heat/ScaledHeatTimePairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous time derivative for the actual scaled heat factors

The derivative uses the actual L2 heat source, with no choice of pointwise time null sets. Compact spatial pairings are treated by the subsequent weak time equation.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_scaled_time_data line 23