OAI/Analysis/RieszRectifiability/Limits/ComplexInteriorCutoffLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the complex interior cutoff

The hard-truncated complex height integrand is the indicator restriction of the full interior integrand to pairs separated by at least the truncation radius. Integrability of the full integrand then yields convergence of the truncated pair integrals as the radii tend to zero.

  1. theorem OAI.RieszRectifiability.complex_height_interior_cutoff_eq_indicator line 21
  2. theorem OAI.RieszRectifiability.complex_height_interior_cutoff_integral_tendsto line 36