OAI/Geometry/RCD/Sobolev/HarmonicEnergyTailBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp local harmonic gradient bounds from a small energy tail

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_energy_small_tail_bound line 14