Commit 2025-09-12 12:47 bbd46d79

View on Github →

feat: a complex differentiable function on a disk has a primitive (#9598) We prove that holomorphic functions on discs have primitives. TODO: Extend to holomorphic functions on simply connected domains, and use this to define general complex logarithms. Co-authored by: Ian Jauslin ian.jauslin@rutgers.edu

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Asymptotics.lean

added theorem Complex.isBigO_im_sub_im

added theorem Complex.isBigO_re_sub_re

Modified Mathlib/Analysis/Complex/Convex.lean

added theorem Complex.Convex.rectangle_subset

modified theorem Complex.isConnected_of_lowerHalfPlane

modified theorem Complex.isConnected_of_upperHalfPlane

added theorem Complex.rectangle_eq_convexHull

Created Mathlib/Analysis/Complex/HasPrimitives.lean

added theorem Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral

added theorem Complex.IsConservativeOn.hasDerivAt_wedgeIntegral

added theorem Complex.IsConservativeOn.isExactOn_ball

added def Complex.IsConservativeOn

added theorem Complex.IsExactOn.isConservativeOn_of_isOpen

added def Complex.IsExactOn

added def Complex.wedgeIntegral

added theorem Complex.wedgeIntegral_add_wedgeIntegral_eq

added theorem DifferentiableOn.isConservativeOn

added theorem DifferentiableOn.isExactOn_ball