OAI/Analysis/CircleDomains/Rigidity/PrincipalRealTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized real-coordinate transfer from the geometric grid

The width, filled real functions and metric used for the energy estimates also give the principal circle model and its genuine transported real functions. The circle model uses only the cited compact metric and finite connectivity uniformization inputs.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_real_coordinate_transfer_from_grid line 23