OAI/Analysis/RieszRectifiability/Limits/DyadicFlatEnergyLimit.lean

Dyadic flat limits with normalized height energy

The flat-measure subsequence construction is augmented with uniform local square and fractional-energy bounds for every normalized normal coordinate. The ball estimates also restrict to bounded projection regions, while the same subsequence retains the convergent plane frames, constant positive planar density, and scalar reflectionlessness of the limit measure.