OAI/Geometry/RCD/Metric/LocalizedPointedConvergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported tests of local pointed value convergence

A fixed gap between the test support and the convergence ball absorbs the metric approximation error. The estimate holds on the whole outer ball.

  1. theorem OAI.RegularPointCoordinates.localized_pointed_uniform_convergence line 18