OAI/Analysis/RieszRectifiability/Limits/OriginalExcessSequenceLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normalized excess for the original sequence

Dyadic excess bounds yield fixed-plane source moments after a finite index shift. Applying the source-excess limit theorem to that tail, then restoring the shift, produces a strictly increasing subsequence with vanishing normalized excess at every nonnegative radius.

  1. theorem OAI.RieszRectifiability.exists_original_excess_sequence_limit line 23