OAI/Analysis/RieszRectifiability/Flatness/LocalFlatBallExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local bilateral flatness in a compact-test limit transfers to nearby support points of the approximating measures, contradicting an eventual lower bound on their local flatness error.

  1. theorem OAI.RieszRectifiability.compactTestConvergence_excludes_local_flat_ball line 19