OAI/Analysis/CircleDomains/Uniformization/ComplexRectangleLocalLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A local rectangular Morera passage, allowing the smooth approximants' poles outside the fixed open set and allowing a finite initial segment.

  1. lemma OAI.CircleDomainRigidity.locally_uniform_curve_integral_on line 13
  2. lemma OAI.CircleDomainRigidity.complexRectangleFlux_tendsto_on line 25
  3. lemma OAI.CircleDomainRigidity.complexRectangleFlux_eq_bar_integral_on line 39
  4. lemma OAI.CircleDomainRigidity.differentiableOn_of_local_rectangle_errors line 59