OAI/Geometry/RCD/Sobolev/FullBochnerCutoffIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cutoff masses of a prescribed full Bochner measure

  1. theorem OAI.RegularPointCoordinates.bochner_energy_identity_of_laplacian line 17
  2. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.full_bochner_mass_identity line 49
  3. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.harmonic_full_mass_identity line 73