OAI/Geometry/RCD/Heat/HeatProductSourceCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two-factor source cancellation for a localized heat bridge

The cutoff-gradient term is retained. It is the boundary error in the local osmotic-energy estimate.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_two_factor_source line 18