OAI/Analysis/RieszRectifiability/Kernel/CommonHeightEquation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common height satisfying renormalized equations

The common subsequential height limit inherits the corrected Riesz equations from uniform local moments and vanishing normalized oscillation. Source-moment tail control further identifies its renormalized pairing on each admissible ball.

  1. theorem OAI.RieszRectifiability.exists_common_height_with_renormalized_equations line 23