OAI/Analysis/RieszRectifiability/Kernel/PairingLocalizationIndependence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Independence of Riesz pairing localization

Exhaustion by outer balls recovers the scalar Riesz pairing from finite restrictions. For compactly supported mean-zero Lipschitz tests, the resulting pairing is independent of the localization center and radius satisfying the support separation bounds.

  1. theorem OAI.RieszRectifiability.ball_subset_outer_of_radius_dist line 21
  2. theorem OAI.RieszRectifiability.restrict_nested_balls_of_subset line 29
  3. theorem OAI.RieszRectifiability.rieszScalarPairing_restrict_outer_ball line 34
  4. theorem OAI.RieszRectifiability.rieszScalarPairing_outer_limit_at_center line 53
  5. theorem OAI.RieszRectifiability.mean_zero_restrict_of_support line 74
  6. theorem OAI.RieszRectifiability.rieszScalarPairing_localization_independent line 80