OAI/Analysis/RieszRectifiability/Limits/DyadicPlanarMeasureLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dyadic planar measure limits

Vanishing dyadic plane moments yield a subsequential AD growth limit supported on a linear plane through the origin. The limit has a bounded intrinsic density, while the convergent frames retain the normal-coordinate moment and local MemLp bounds.

  1. theorem OAI.RieszRectifiability.exists_dyadic_planar_measure_limit line 25