OAI/Geometry/RCD/Sobolev/WeightedEnergyLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sharp lower bounds for compactly weighted energies

The weight is an actual test on the prescribed approximation maps. The subsequence uses the same positive energy measures as the unweighted proof.

  1. theorem OAI.RegularPointCoordinates.euclideanBallProbability_absolutelyContinuous line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.weighted_energy_lower_of_curvature_sequence line 35