Existing in Mathlib · Complex analysis
Maximum Modulus Principle
If the norm of a complex-differentiable map reaches its maximum at an interior point of an open preconnected domain, then that norm has the same value everywhere on the domain.
- maximum modulus principle
- complex differentiability
- preconnected sets
- local maxima
- open-set separation
- constant norm
Exact theorem
Exact Mathlib statement
theorem norm_eqOn_of_isPreconnected_of_isMaxOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : EqOn (norm ∘ f) (const E ‖f c‖) UThe theorem at a glance
Maximum Modulus Principle at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Maximum Modulus Principle at a glance
Detailed visual description
The poster states the exact equality-of-norms conclusion, traces the checked route through an open maximum-level set V and an open unequal-norm set W, and uses preconnectedness to force U into V. The closing abstract codomain surface keeps several image values distinct while placing them on one common norm boundary, emphasizing that the selected theorem does not say f itself is constant.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
One connected domain, one common norm shell
Detailed visual description
One irregular haloed domain contains a gold distinguished interior point and three other interior points connected by a sparse path network. Four strands carry those sources to a gold circle, green square, purple triangle, and vermilion diamond placed at equal radius around one neutral center. The shared radius represents constant norm; the distinct shapes prevent an equality-of-values reading.
Why it matters
A mathematical landmark
The maximum modulus principle is a fundamental rigidity theorem of complex analysis. This Mathlib endpoint makes its connectedness mechanism unusually explicit: local analytic rigidity and continuity create two open alternatives, and preconnectedness forces the norm to remain at its attained maximum everywhere.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's equality-of-norms form of the maximum modulus principle on an open preconnected set. For complex normed spaces E and F, a complex-differentiable map f on U, and an interior point c where ‖f ·‖ is maximal on U, it concludes ‖f x‖ = ‖f c‖ throughout U. It does not conclude that the values f x are equal, and it does not state the nearby strictly-convex-codomain, closure, frontier, or local-maximum variants.
- The selected declaration proves equality of the norms ‖f x‖ and ‖f c‖; it does not prove equality of the values f x and f c.
- The stronger equality-of-values declaration for a strictly convex codomain is a separate nearby theorem and is not the endpoint indexed here.
- The selected theorem concerns U itself, not closure U or frontier U, and it is not the local-maximum or closed-ball formulation.
- The assumptions that U is open and preconnected, that c lies in U, and that f is complex differentiable on U are part of the exact statement.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Complex.norm_eqOn_of_isPreconnected_of_isMaxOnin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.maximum-modulus-principle.v001