OAI/Analysis/CircleDomains/Transfer/AssembledRealTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Real finite transfer from the original coordinate data

The regular core, reciprocal grid, physical terminal disks, remaining fillings, common metric and principal circle model are selected together. Both the localized energy inequality and the physical terminal excess refer to these same choices.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_assembled_real_transfer line 26