OAI/Analysis/CircleDomains/Rigidity/PreparedMaskAtlasGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Select one regular core, cutoff and reciprocal grid for the actual finite masked list, then construct its terminal and subordinate filling caps using that very grid. All cost and terminal estimates retain these same choices.

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