OAI/Analysis/RieszRectifiability/Limits/FixedCutoffPairingLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-cutoff limits of hard-truncated pairings

Restricting a globally growing measure to the outer ball gives a finite measure. Mean-zero Lipschitz tests then identify the limit of dyadic hard truncations with the scalar Riesz pairing on that restriction. The ball indicator also has finite squared integral equal to the real mass of the ball.

  1. theorem OAI.RieszRectifiability.fixed_cutoff_hard_pairing_limit line 22
  2. theorem OAI.RieszRectifiability.ball_indicator_one_memLp_and_sq_integral line 55