OAI/Analysis/CircleDomains/Rigidity/MatchedRealMaskConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of every mask system, including its actual L² paying density, continuous compact scalar, and connected residual-dust domain.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.exists_real_mask line 16