OAI/Geometry/RCD/Heat/HeatPowerEnergyBalance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the mixed energy in a heat-bridge power

The two actual L2 sources are paired against bounded Sobolev powers. The mixed Gamma terms cancel without any derivative of either source.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_power_energy_balance line 18