OAI/Geometry/RCD/Sobolev/PositiveEnergyExcess.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong energy-density comparison transfers a sharp upper bound

  1. theorem OAI.RegularPointCoordinates.square_positive_excess_le line 12
  2. theorem OAI.RegularPointCoordinates.positive_energy_excess_tendsto line 21