OAI/Analysis/CircleDomains/Selection/WedgeMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Averaging the cutoff wedge estimate

Independent shifts reduce the leading wedge term to its original size. The error from the common cutoff is linear in the grid spacing. Integrals here use the square of shifts before normalization by its area h².

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_cutoff_wedge_le line 18