OAI/Geometry/RCD/Harmonic/EventualQuadraticError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Square-root errors from uniform Young estimates

The free Young parameter may be chosen after the mass budget. The choice also works when the limiting mass is zero.

  1. theorem OAI.RegularPointCoordinates.eventual_error_le_sqrt line 17
  2. theorem OAI.RegularPointCoordinates.eventual_error_le_sqrt_add line 33