OAI/Geometry/RCD/Sobolev/WeightedGammaL2Continuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

L²-weight continuity with a uniform gradient bound

Clip the weight, pass the bounded-weight Sobolev limit, and control the tail with the common gradient bound. The test needs only Sobolev regularity.

  1. theorem OAI.RegularPointCoordinates.weightedGamma_weight_difference line 22
  2. theorem OAI.RegularPointCoordinates.weightedGamma_fixed_weight_tendsto line 29