OAI/Analysis/CircleDomains/Topology/RealModelExhaustion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exhausting real transfer models

The prescribed source sets and the common exterior are constructed from the domain. Thus the normal-family hypotheses follow from the actual finite transfers, rather than being extra assumptions on their maps.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_real_model_exhaustion line 46
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.core_model line 107
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.core_conformal line 115
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.exists_conformal_limit line 123