OAI/Geometry/RCD/Sobolev/BochnerCutoffFlux.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the full Bochner source against an actual Laplacian cutoff

The source is only Sobolev and L². Multiplication by the compact Lipschitz cutoff gives an admissible test without a bounded-source assumption.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_cutoff_source_flux line 20
  2. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.bochner_source_identity line 57