OAI/Analysis/CircleDomains/Rigidity/MaskedGridPreparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Preparing the actual masked circle transfer

The regular core contains every mask boundary, the cutoff is constructed, and the actual reciprocal grid and good widths are selected from the original masked L² data. No modified-coordinate integrability is assumed.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_maskedCircleWedges_eq_intersections line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_regular_masked_core_cutoff_and_grid line 39