Morera's theorem #
This file provides the named scalar form of Morera's theorem required by the L0 target
"Morera as a named theorem" in TauCetiRoadmap/ConformalMapping/README.md. Mathlib already
proves the more general equivalence between conservativity and complex differentiability, so
the result here is a direct specialization rather than a parallel API.
Main results #
TauCeti.morera: a continuous function on an open set whose rectangle integrals vanish is holomorphic.
Coordination with upstream Mathlib #
The conformal-mapping roadmap's L0-L3 layers overlap the in-progress Riemann mapping work in
mathlib4#33505. If Mathlib adds a
dedicated morera declaration, this named specialization should be refactored onto it.
References #
- L. Ahlfors, Complex Analysis, Ch. 4, Section 6.
- J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IV, Section 5.
theorem
TauCeti.morera
{U : Set ℂ}
{f : ℂ → ℂ}
(hU : IsOpen U)
(hcont : ContinuousOn f U)
(hcons : Complex.IsConservativeOn f U)
:
DifferentiableOn ℂ f U
Morera's theorem. A continuous function on an open set whose rectangle integrals vanish is holomorphic.