Complex analysis
Complex Fréchet differentiability on open subsets of finite-dimensional complex normed spaces implies local analyticity for maps into complete complex normed spaces. The proof uses an iterated polydisc Cauchy formula, analytic continuous-function-valued kernels, and bounded vector-valued integration. The integration API is independently importable.
Quoted from the project description in formalization.yaml of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
7 articles: 7 for headline results in its README whose declaration link names a declaration the scan finds in the linked file.
Facts
From the repository and its formalization.yaml; the review and automation statements are quoted as written.
- Repository: FormalFrontier/complex-analysis, read at commit c22c803e (2026-11-04).
- Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
- License: Apache-2.0.
- Authors: Formal Frontier Agents.
- Review status: “agent-reviewed”.
- Automation: agent; framework “Codex and Hive”; prompting notes “Agent-assisted mathematical formalization using Mathlib.”
Literature
The sources its formalization.yaml names, with their relationship to it.
- The classical Cauchy integral formula on polydiscs (folklore; independently-proves).
Builds on
- Polynomial root stability (a Lake dependency, pinned at 545e66a4)
- Sphere topology (a Lake dependency, pinned at 4b3c3b4a)
Used by
Headline results
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
TheoremFinite-dimensional differentiability implies analyticity#
A complex Fréchet-differentiable map on an open subset of a finite-dimensional complex normed space is analytic near every point of that set, when its target is a complete complex normed space; dimension zero is included.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
DifferentiableOn.analyticOnNhd_of_finiteDimensional(theorem), declared in ComplexAnalysis/Analysis/Complex/FiniteDimensional.lean, line 49.
Read from the source at commit c22c803e, without running Lean.
Sources
TheoremDifferentiability–analyticity equivalence#
On such an open set, analyticity near every point is equivalent to complex Fréchet differentiability, under the same source and target hypotheses.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
analyticOnNhd_iff_differentiableOn_of_finiteDimensional(theorem), declared in ComplexAnalysis/Analysis/Complex/FiniteDimensional.lean, line 87.
Read from the source at commit c22c803e, without running Lean.
Sources
TheoremPolydisc Cauchy formula#
A complex-differentiable map on a positive-radius closed coordinate polydisc, valued in a complete complex normed space, agrees at interior points with its normalized torus boundary integral.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
DifferentiableOn.torusIntegral_cauchy(theorem), declared in ComplexAnalysis/Analysis/Complex/TorusCauchy.lean, line 86.
Read from the source at commit c22c803e, without running Lean.
Sources
TheoremPolynomial boundary degree counts interior roots#
A complex polynomial with no zeros on the unit circle gives an unbased continuous circle self-map by normalizing its values. Its degree equals the number of roots strictly inside the unit disk, counted with multiset multiplicity. Nonmonic polynomials, repeated roots and nonzero constants of arbitrary phase are included.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
Polynomial.degree_normalizedCircleMap(theorem), declared in ComplexAnalysis/Analysis/Complex/PolynomialBoundary.lean, line 231.
Read from the source at commit c22c803e, without running Lean.
Sources
DefinitionExterior polynomial root-scaling homotopy#
If p.eval w ≠ 0 whenever 1 ≤ ‖w‖, root scaling over the real unit interval
joins the normalized leading monomial to the canonical normalized boundary map.
Its characteristic value is normalize ((p.scaleRoots (t : ℂ)).eval z).
The leading coefficient's arbitrary phase is retained; the corresponding degree
statement is Circle.degree (p.normalizedCircleMap _) = (p.natDegree : ℤ).
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
Polynomial.normalizedCircleMapScaleRootsHomotopy(def), declared in ComplexAnalysis/Analysis/Complex/PolynomialExterior.lean, line 58.
Read from the source at commit c22c803e, without running Lean.
Sources
DefinitionCompact scalar-kernel operators#
A continuous scalar kernel on X × Y, with compact Y and a finite Borel
measure, gives a compact complex-linear map from L²(Y, μ) to C(X, ℂ).
The parameter space X is arbitrary; compactness of X is needed only for
the sup-norm bound. The construction uses a generic transpose of an
operator-norm-continuous field, compact whenever its normed target is proper.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
ContinuousMap.kernelOperator(def), declared in ComplexAnalysis/MeasureTheory/Integral/Kernel.lean, line 218.
Read from the source at commit c22c803e, without running Lean.
Sources
TheoremDetecting finite eigenspaces of compact positive squares#
On an arbitrary complete real or complex Hilbert space, compact T and
continuous linear B with B.comp T ≠ 0 give a nonzero eigenvalue of
T.comp T.adjoint whose finite-dimensional eigenspace contains a vector
v with B v ≠ 0. No separability or commutation hypothesis is needed.
Quoted from the headline results in README.md of FormalFrontier/complex-analysis at commit c22c803e, Apache-2.0.
Lean
ContinuousLinearMap.exists_eigenvector_comp_adjoint_detected(theorem), declared in ComplexAnalysis/Analysis/InnerProductSpace/CompactOperator.lean, line 69.
Read from the source at commit c22c803e, without running Lean.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.