OAI/Geometry/RCD/Sobolev/BochnerMixedTerm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the mixed term in weak Bochner

Testing the weak Laplacian against the product of its derivative and a bounded Sobolev weight moves the mixed term onto the weight. This is the identity needed for an energy bound depending only on the L² Laplacian.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_mixed_weight_identity line 21