OAI/Analysis/CircleDomains/Sobolev/LocalComplexWeyl.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local Weyl lemma for the actual weak complex differential. Positive mollification preserves the Cauchy–Riemann equations on smaller compact sets, and locally uniform convergence identifies the holomorphic limit.

  1. theorem OAI.CircleDomainRigidity.complexifyPair_mollification_tendsto line 17
  2. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.mollified_differentiableAt line 49
  3. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.holomorphic_on_of_cauchyRiemann line 77