OAI/Geometry/RCD/Harmonic/WeightedAffinePotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted scalar potentials with a nonzero derivative at zero

The weight also belongs to L², so the affine term has a genuine bounded linear derivative. No constant function is placed in L² on an infinite measure space.

  1. theorem OAI.RegularPointCoordinates.weightedIntegralPotential_affine_hasFDerivAt line 18