OAI/Analysis/CircleDomains/Reflection/CompactDiffeomorphismBeltrami.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A smooth plane diffeomorphism fixed near infinity has an actual smooth, compactly supported complex dilatation, uniformly bounded strictly below one.

  1. lemma OAI.CircleDomainRigidity.smooth_homeomorph_fderiv_injective line 14
  2. lemma OAI.CircleDomainRigidity.smooth_homeomorph_wirtinger_gap_ne_zero line 26
  3. lemma OAI.CircleDomainRigidity.homeomorph_partials_eq_id_off line 35
  4. lemma OAI.CircleDomainRigidity.compact_diffeomorphism_wirtinger_gap_pos line 44
  5. lemma OAI.CircleDomainRigidity.compact_diffeomorphism_beltrami line 64