OAI/Analysis/CircleDomains/Rigidity/PrincipalMaskedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Principally normalized actual masked finite transfer

The selected cutoff and filled metric produce a normalized finite circle model with its smooth inverse and actual transported coordinates. The source energy estimates and exact target energy formula hold for the same width, metric, model and coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_actual_masked_transfer line 24