OAI/Geometry/RCD/Harmonic/QuadraticErrorL1Limit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An integrable quadratic error bound implies local L1 convergence

This is the final scalar estimate used for mixed Hessian errors. The gradient error enters through its integral against the fixed density.

  1. theorem OAI.RegularPointCoordinates.quadratic_error_L1_limit line 18