Maximum Modulus Principle

Statement

Let $f$ be holomorphic on a connected open set $U$ and continuous on $\overline{U}$. If $f$ is not constant, then $|f|$ attains its maximum only on the boundary $\partial U$:

Equivalently: if $|f|$ has a local maximum at an interior point $c \in U$, then $f$ is constant near $c$ (and by the Identity Theorem, everywhere on $U$).

Visualization

$f(z) = z^2$ on the unit disk $|z| \le 1$.

| $z$ | $|z|$ | $|f(z)| = |z^2|$ | |-----|-------|-----------------| | $0$ | $0$ | $0$ | | $0.5$ | $0.5$ | $0.25$ | | $i \cdot 0.7$ | $0.7$ | $0.49$ | | $e^{i\pi/4}$ | $1$ | $1$ | | $1$ | $1$ | $1$ | | $-1$| $1$ | $1$ |

The maximum of $|z^2|$ on $|z| \le 1$ is $1$, attained on the boundary circle $|z| = 1$ — never at an interior point where $|z| < 1$.

  Boundary |z|=1: |f| = 1 everywhere (maximum)
  
       -i
       |
  -1---+---1    <-- boundary circle: |f| = 1
       |
       i
  
  Interior: |f(z)| = |z|^2 < 1 for |z| < 1

Proof Sketch

1. Suppose $|f(c)| \ge |f(z)|$ for all $z$ in some disk $B(c, r) \subset U$.
2. The Cauchy integral formula gives $f(c) = \frac{1}{2\pi}\int_0^{2\pi} f(c + re^{i\theta})\,d\theta$ (mean value property).
3. Taking moduli: $|f(c)| \le \frac{1}{2\pi}\int_0^{2\pi}|f(c + re^{i\theta})|\,d\theta \le |f(c)|$.
4. Equality forces $|f(c + re^{i\theta})| = |f(c)|$ for almost every $\theta$ — a constant modulus on the circle.
5. A holomorphic function with constant modulus on any disk is itself constant (open mapping or CR equations). So $f$ is constant near $c$, hence everywhere by analytic continuation.

Connections

The Maximum Modulus Principle gives Liouville's TheoremLiouville's Theorem$$f : \mathbb{C} \to \mathbb{C} \text{ entire},\; |f| \leq C \implies f \equiv \text{const}$$A bounded entire function on ℂ must be constant — complex differentiability is far more rigid than real differentiabilityRead more → immediately (a bounded entire function is constant: take $U$ to be a large disk). It is closely related to the Cauchy Integral FormulaCauchy Integral Formula$$f(w) = \frac{1}{2\pi i}\oint_{|z-c|=R} \frac{f(z)}{z - w}\,dz$$A holomorphic function's value at any interior point is determined by its values on the boundary circle.Read more → via the mean-value property. For real-valued functions, the analogous result is the Mean Value TheoremMean Value Theorem$$\exists\, c \in (a,b)\;:\; f'(c) = \frac{f(b)-f(a)}{b-a}$$There exists a point where the instantaneous rate of change equals the average rate of changeRead more → for harmonic functions.

import Mathlib.Analysis.Complex.AbsMax

open Complex

/-- **Maximum Modulus Principle**: on a preconnected open set, if |f| achieves
    its maximum at an interior point, then |f| is constant on the closure.
    Uses `Complex.norm_eqOn_of_isPreconnected_of_isMaxOn` from Mathlib. -/
theorem maximum_modulus_principle {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {U : Set ℂ} {f : ℂ → E} {c : ℂ}
    (hc : IsPreconnected U) (hU : IsOpen U)
    (hf : DifferentiableOn ℂ f U)
    (hcU : c ∈ U)
    (hmax : IsMaxOn (‖f ·‖) U c) :
    ∀ x ∈ U, ‖f x‖ = ‖f c‖ :=
  fun x hx => norm_eqOn_of_isPreconnected_of_isMaxOn hc hU hf hcU hmax hx