OAI/Analysis/CircleDomains/Uniformization/ScalarModelInverseConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual continuous projections of finite scalar models converge to the inverse on the limiting conformal image. This also transports uniformly convergent source tests to their actual model continuations.

  1. theorem OAI.CircleDomainRigidity.CompactScalarCircleModel.projection_finite line 16
  2. theorem OAI.CircleDomainRigidity.scalar_model_projection_tendsto line 24
  3. theorem OAI.CircleDomainRigidity.scalar_model_continuations_tendsto line 64