OAI/Geometry/RCD/Sobolev/HarmonicL1GradientBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sharp inner gradients from the actual outer L1 energy error

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_unit_tail_bound line 15
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_l1_gradient_bound line 86