OAI/Geometry/RCD/Harmonic/SignedRadialWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Signed radial exponential weights for the Davies estimate

Both signs of the bounded distance weight are needed when the two half-time density rows are paired. No heat-kernel estimate is assumed.

  1. theorem OAI.RegularPointCoordinates.radialWeight_signed_bound line 19
  2. theorem OAI.RegularPointCoordinates.radialWeight_signed_lipschitz line 27
  3. theorem OAI.RegularPointCoordinates.radialWeight_signed_slope line 52
  4. theorem OAI.RegularPointCoordinates.heatAt_signed_radialWeight_integral line 74