OAI/Analysis/CircleDomains/Rigidity/ActualMaskedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the selected actual masked cutoff

The collar construction and the common-width energy selection are applied to the actual reciprocal-grid cutoff family. Only the original masked L² norms are used on the retained core.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.transfer_actual_masked_circle_cutoff line 20