OAI/Analysis/RieszRectifiability/Nets/HeightBallRadiusIndependence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Independence of the height-pairing radius

Local square integrability and a weighted tail bound make the renormalized far pairing integrable. Local fractional energy then permits comparison through common outer balls, showing that a mean-zero compact test gives the same height pairing for either admissible localization radius.

  1. theorem OAI.RieszRectifiability.renormalized_far_integrable_of_ball_L2 line 24
  2. theorem OAI.RieszRectifiability.heightPairingOn_ball_independent_from_local_energy line 43