OAI/Analysis/CircleDomains/Reflection/SchwarzReflection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Schwarz reflection across a real interval, with continuity and holomorphy proved for the actual piecewise extension.

  1. def OAI.CircleDomainRigidity.schwarzReflect line 14
  2. lemma OAI.CircleDomainRigidity.schwarzReflect_eq line 17
  3. lemma OAI.CircleDomainRigidity.continuousOn_schwarzReflect line 20
  4. lemma OAI.CircleDomainRigidity.differentiableOn_schwarzReflect line 37
  5. lemma OAI.CircleDomainRigidity.schwarzReflect_conj line 56