OAI/Geometry/RCD/Sobolev/PoissonGradientFromScalar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact gradient-product input from scalar dimensional Bochner

The regular test algebra is dense. Testing against a compactly localized copy of the actual mixed gradient proves the full Sobolev energy estimate. No Laplacian or Lipschitz premise is imposed on that mixed representative.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_gradient_product_input_of_scalar line 24