OAI/Analysis/RieszRectifiability/Projections/GlobalProjectionLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global projection heights

Countable projection limits agree on open overlaps and glue to a measurable height on the coordinate plane. The common subsequence preserves local second moments and pairings with compactly supported Lipschitz tests.

  1. theorem OAI.RieszRectifiability.exists_global_projection_height line 23