OAI/Geometry/RCD/Sobolev/CompactBochnerTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bochner positivity for compact Lipschitz functions with L² Laplacian

The mixed derivative is integrated by parts before taking the heat-time limit. Only the L² Laplacian occurs in the resulting formula.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_bochner_sobolev_test line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_bochner_test line 104