OAI/Geometry/RCD/Sobolev/WeakLaplacianFluxIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact weak flux of a forward/backward heat product

Two weak Laplacians tested against actual bounded Sobolev products give the antisymmetric flux identity. All terms remain in the original measure.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_bounded_product_test line 18
  2. theorem OAI.RegularPointCoordinates.weakLaplacian_product_flux line 44