OAI/Analysis/CircleDomains/Rigidity/MaskedGridSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common grid selection from masked L² fields

The correction terms are integrated only where both coordinates are present. Their finite sum is independent of width. Shrinking the grid spacing therefore permits the same terminal-count and good-width selection used for globally defined coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_for_masked_wedge_cost line 21