OAI/Analysis/CircleDomains/Uniformization/ExteriorCoefficientBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The published coefficient area theorem and exterior bounds

Ahlfors, Conformal Invariants (1973), Theorem 5-1, p. 83, states that the Laurent coefficients of a normalized exterior univalent map satisfy the weighted square-sum bound. The proposition below includes its Laurent expansion, in the zero-constant-term normalization needed here. It is an explicit published input.

Only a coarse uniform exterior bound is needed for normal-family compactness. It follows from the coefficient inequality and a geometric series, with no additional analytic input.

  1. def OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem line 26
  2. theorem OAI.CircleDomainRigidity.norm_coefficient_le_one line 33
  3. theorem OAI.CircleDomainRigidity.norm_exterior_series_le_one line 42
  4. theorem OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem.exterior_bound line 61