OAI/Analysis/CircleDomains/Uniformization/ComplexRectangleLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rectangular Morera passage for smooth maps with vanishing antiholomorphic error. Uniform convergence is needed only on the four compact edges.

  1. def OAI.CircleDomainRigidity.complexRectangleFlux line 14
  2. lemma OAI.CircleDomainRigidity.locally_uniform_curve_integral line 18
  3. lemma OAI.CircleDomainRigidity.complexRectangleFlux_tendsto line 28
  4. lemma OAI.CircleDomainRigidity.complexRectangleFlux_eq_bar_integral line 37
  5. lemma OAI.CircleDomainRigidity.differentiableOn_of_vanishing_rectangle_errors line 57