OAI/Analysis/CircleDomains/Reflection/HolomorphicAcrossRealAxis.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A continuous complex function holomorphic off the real axis is holomorphic across it. Rectangles are split at the axis and their common horizontal integrals cancel. This is the gluing step needed for Schwarz reflection, proved directly from Cauchy--Goursat.

  1. def OAI.CircleDomainRigidity.rectangleFlux line 14
  2. lemma OAI.CircleDomainRigidity.rectangleFlux_one_side line 18
  3. lemma OAI.CircleDomainRigidity.vertical_integrable line 32
  4. lemma OAI.CircleDomainRigidity.rectangleFlux_split line 41
  5. lemma OAI.CircleDomainRigidity.rectangleFlux_off_real line 58
  6. lemma OAI.CircleDomainRigidity.differentiableOn_of_continuousOn_off_real line 79