OAI/Analysis/RieszRectifiability/Limits/RenormalizedLimitEquation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Renormalized equation from source moments

Local square-integrability and inherited source-moment tail bounds make the renormalized height pairing integrable. Exhaustion by bounded projection regions then turns the vanishing limiting bilinear pairings into a zero ball pairing.

  1. theorem OAI.RieszRectifiability.renormalized_limit_equation_from_source_moments line 23