OAI/Geometry/RCD/Sobolev/ShiftedDensityCutoffBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative inner bounds from the full shifted cutoff mass

No absolute continuity of the full Bochner measure is needed. Its singular part contributes with the correct sign to the upper bound.

  1. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.shifted_density_le_full line 18
  2. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.shifted_inner_density_le line 46
  3. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.shifted_inner_density_eventually_le line 67