OAI/Analysis/CircleDomains/Transfer/ActualMixedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer real barriers and masked period coordinates using one width and one metric, retaining the exact real barriers near the chosen core.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.transfer_actual_mixed_cutoff line 14