OAI/Analysis/CircleDomains/Rigidity/MaskedCircleFillings.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Circle fillings with coordinate-specific masks

Real collar branches still give one simultaneous rank-one filling. Smoothness is required only on each coordinate's own mask. The common boundary agreement and zero-wedge identities hold on all filling disks.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.IsMaskedFilledCircleFamily line 22
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_masked_filled_circle_coordinates line 28
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_fill_actual_masked_circle_cutoff line 94
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsMaskedFilledCircleFamily.masked_wedges_eq_zero line 130
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsMaskedFilledCircleFamily.masked_wedges_eq_outside line 143