OAI/Analysis/CircleDomains/Reflection/ActualPhaseReflection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit bounded holomorphic reflections of the actual fixed-phase cumulative maps on their common source collar.

  1. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.reflected line 16
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.reflected_holomorphic line 20
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.reflected_injective line 28
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.reflected_bounded line 35
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.reflected_agrees line 42
  6. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.exists_reflected_limit line 50