OAI/Analysis/RieszRectifiability/Limits/HeightPairingOuterLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Outer exhaustion and localization of the height pairing

Restricting to expanding outer balls leaves the local bilinear term unchanged and exhausts the integrable renormalized far term. Equality of the finite-region pairings then passes to the limit, proving independence of the localization region for the same supported, mean-zero test function.

  1. theorem OAI.RieszRectifiability.restrict_set_inside_ball line 22
  2. theorem OAI.RieszRectifiability.heightPairingOn_restrict_outer_ball line 27
  3. theorem OAI.RieszRectifiability.heightPairingOn_outer_limit line 44
  4. theorem OAI.RieszRectifiability.center_height_integrable_finite_region line 64
  5. theorem OAI.RieszRectifiability.heightPairingOn_localization_independent line 78