OAI/Geometry/RCD/Heat/ScaledHeatJointEquation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous time source equals the local Sobolev equation

The pointwise continuous source and all compact Sobolev realizations are identified by uniqueness of the actual time derivative.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_scaled_joint_equation line 21