OAI/Analysis/RieszRectifiability/Foundations/HardExteriorOscillation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exterior oscillation of hard truncations

Global upper growth controls the integral of a bounded density times a far-field kernel difference. For an L² density supported outside a ball, this gives the corresponding oscillation estimate for the exact hard-truncated transform.

  1. theorem OAI.RieszRectifiability.bounded_exterior_kernel_difference line 21
  2. theorem OAI.RieszRectifiability.truncated_eq_exterior_integral_of_support line 59
  3. theorem OAI.RieszRectifiability.hard_truncated_exterior_difference_bound line 80