OAI/Analysis/RieszRectifiability/Limits/OriginalBilateralSequenceLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bilateral flatness along a subsequence

Vanishing dyadic excess and scalar oscillation yield a planar weak limit after shifting and extracting a subsequence. Lower mass bounds then turn this planar limit into convergence of the original measures' bilateral beta numbers at every fixed positive radius.

  1. theorem OAI.RieszRectifiability.exists_original_bilateral_sequence_limit line 24