Maximum modulus principle #

In this file we prove several versions of the maximum modulus principle. There are several statements that can be called "the maximum modulus principle" for maps between normed complex spaces. They differ by assumptions on the domain (any space, a nontrivial space, a finite dimensional space), assumptions on the codomain (any space, a strictly convex space), and by conclusion (either equality of norms or of the values of the function).

Main results #

Theorems for any codomain #

Consider a function f : E → F that is complex differentiable on a set s, is continuous on its closure, and ‖f x‖ has a maximum on s at c. We prove the following theorems.

Complex.norm_eqOn_closedBall_of_isMaxOn: if s = Metric.ball c r, then ‖f x‖ = ‖f c‖ for any x from the corresponding closed ball;
Complex.norm_eq_norm_of_isMaxOn_of_ball_subset: if Metric.ball c (dist w c) ⊆ s, then ‖f w‖ = ‖f c‖;
Complex.norm_eqOn_of_isPreconnected_of_isMaxOn: if U is an open (pre)connected set, f is complex differentiable on U, and ‖f x‖ has a maximum on U at c ∈ U, then ‖f x‖ = ‖f c‖ for all x ∈ U;
Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn: if s is open and (pre)connected and c ∈ s, then ‖f x‖ = ‖f c‖ for all x ∈ closure s;
Complex.norm_eventually_eq_of_isLocalMax: if f is complex differentiable in a neighborhood of c and ‖f x‖ has a local maximum at c, then ‖f x‖ is locally a constant in a neighborhood of c.

Theorems for a strictly convex codomain #

If the codomain F is a strictly convex space, then in the lemmas from the previous section we can prove f w = f c instead of ‖f w‖ = ‖f c‖, see Complex.eqOn_of_isPreconnected_of_isMaxOn_norm, Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm, Complex.eq_of_isMaxOn_of_ball_subset, Complex.eqOn_closedBall_of_isMaxOn_norm, and Complex.eventually_eq_of_isLocalMax_norm.

Values on the frontier #

Finally, we prove some corollaries that relate the (norm of the) values of a function on a set to its values on the frontier of the set. All these lemmas assume that E is a nontrivial space. In this section f g : E → F are functions that are complex differentiable on a bounded set s and are continuous on its closure. We prove the following theorems.

Complex.exists_mem_frontier_isMaxOn_norm: If E is a finite dimensional space and s is a nonempty bounded set, then there exists a point z ∈ frontier s such that (‖f ·‖) takes it maximum value on closure s at z.
Complex.norm_le_of_forall_mem_frontier_norm_le: if ‖f z‖ ≤ C for all z ∈ frontier s, then ‖f z‖ ≤ C for all z ∈ s; note that this theorem does not require E to be a finite dimensional space.
Complex.eqOn_closure_of_eqOn_frontier: if f x = g x on the frontier of s, then f x = g x on closure s;
Complex.eqOn_of_eqOn_frontier: if f x = g x on the frontier of s, then f x = g x on s.

Tags #

maximum modulus principle, complex analysis

Auxiliary lemmas #

We split the proof into a series of lemmas. First we prove the principle for a function f : ℂ → F with an additional assumption that F is a complete space, then drop unneeded assumptions one by one.

The lemmas with names *_auxₙ are considered to be private and should not be used outside of this file.