OAI/Geometry/RCD/Sobolev/BochnerMassExponential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exponential envelopes for the quantitative local Bochner masses

  1. theorem OAI.RegularPointCoordinates.radial_mass_bound_le_exp line 14