OAI/Geometry/RCD/Metric/LocalizedMeasuredValueLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak value limits against compactly supported Lipschitz tests

Uniform local convergence controls the source error on the full outer ball. The remaining fixed test is covered by the measured approximation itself.

  1. theorem OAI.RegularPointCoordinates.localized_measured_value_limit line 18