OAI/Geometry/RCD/Sobolev/HarmonicGradientConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local harmonic gradient input from the RCD structure

Nonpositive curvature uses the constructed scalar Bochner estimate. Positive curvature uses the proved RCD(0,n) reduction; the required bounded-curvature gradient estimate transfers to the original space.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonicGradientInput_nonpositive line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonicGradientInput line 34