Complex Analysis

Cauchy Integral Formula

A holomorphic function's value at any interior point is determined by its values on the boundary circle.

lean4-proofcomplex-analysisvisualization

Residue Theorem

A contour integral of a meromorphic function equals 2πi times the sum of residues of enclosed poles.

lean4-proofcomplex-analysisvisualization

Maximum Modulus Principle

A non-constant holomorphic function on a connected open set cannot attain its maximum modulus at an interior point.

lean4-proofcomplex-analysisvisualization

Schwarz Lemma

A holomorphic self-map of the unit disk fixing the origin satisfies |f(z)| ≤ |z| and |f'(0)| ≤ 1.

lean4-proofcomplex-analysisvisualization

Morera's Theorem

A continuous function whose integral vanishes on every rectangle in a disk is holomorphic.

lean4-proofcomplex-analysisvisualization

Identity Theorem (Analytic Continuation)

Two analytic functions on a connected domain that agree on a set with a limit point must be identical.

lean4-proofcomplex-analysisvisualization

Open Mapping Theorem (Complex)

A non-constant holomorphic function on a connected open set maps open sets to open sets.

lean4-proofcomplex-analysisvisualization

Argument Principle

The winding number of f around 0 along a contour equals the number of zeros minus poles enclosed.

lean4-proofcomplex-analysisvisualization

Liouville's Theorem

A bounded entire function on ℂ must be constant — complex differentiability is far more rigid than real differentiability

lean4-proofcomplex-analysisvisualization

Fundamental Theorem of Algebra

Every non-constant polynomial with complex coefficients has at least one root in ℂ

lean4-proofcomplex-analysisvisualization