OAI/Analysis/CircleDomains/Modulus/TerminalCollarOscillation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform oscillation on target collars, derived from the proved assignment of target ends to physical terminal boundaries. No boundary extension of the uniformizing map is assumed.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.inverse_boundary_neighborhood line 18
  2. theorem OAI.CircleDomainRigidity.exists_open_oscillation_bound line 38
  3. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.round_collar_oscillation line 61