Existing in Mathlib · Complex analysis
Liouville's Theorem
Let E and F be complex normed vector spaces, and let f map all of E into F. If f is complex differentiable everywhere and its entire range stays bounded, then every input has exactly the same output.
- complex differentiability
- bounded range
- entire map
- constant function
- complex normed spaces
Exact theorem
Exact Mathlib statement
theorem Differentiable.exists_eq_const_of_bounded {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (Set.range f)) : ∃ c : F, f = Function.const E cThe theorem at a glance
Liouville's theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Liouville's theorem at a glance
Detailed visual description
The poster separates the unbounded input space, global differentiability, bounded output range, and constant conclusion. A Cauchy-estimate route visually lets the derivative bound shrink as radius grows, without restricting the headline theorem to scalar functions.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Liouville's theorem schematic
Detailed visual description
A broad, unbounded domain E carries many sample points and complex directions. Their smooth map paths enter one bounded contour in F and terminate at the same point c, emphasizing normed-space generality rather than only a complex-plane graph.
Why it matters
A mathematical landmark
Liouville's theorem converts a global growth restriction into complete rigidity. It is a central tool in complex analysis and a standard bridge to the Fundamental Theorem of Algebra.
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 target indexes Mathlib's complex Fréchet-differentiable normed-space theorem: E and F are complex normed spaces, f is differentiable on all of E, and its range is bounded. The conclusion is exact equality with a constant function. The declaration is more general than the scalar ℂ→ℂ slogan and does not require F to be complete.
- Proof Atlas did not originate Liouville's theorem or Mathlib's declaration.
- The selected endpoint is not restricted to scalar-valued functions on the complex plane.
- The theorem does not apply to a function assumed differentiable only on a proper bounded domain.
- This is not Liouville's number-theoretic approximation theorem.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Differentiable.exists_eq_const_of_boundedin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.liouville-theorem.v001