OAI/Analysis/CircleDomains/Uniformization/CircuitUniformError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence on a source circuit gives a vanishing numerical error bound. No regularity of the finitely many early models is needed.

  1. theorem OAI.CircleDomainRigidity.exists_circuit_uniform_error line 14
  2. theorem OAI.CircleDomainRigidity.tendstoUniformlyOn_retained_circuit line 50