OAI/Analysis/CircleDomains/Uniformization/FiniteModelTerminalEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Terminal estimates on an actual finite circle model

The terminal assignment is constructed from the smooth model. The same branches produced on physical terminal collars have the required summed cluster-oscillation bound at their assigned target components.

  1. theorem OAI.CircleDomainRigidity.exists_finite_model_terminal_estimates line 22