mathlib documentation

analysis.complex.abs_max

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.

In the most general case, see complex.norm_eventually_eq_of_is_local_max, we can only say that for a differentiable function f : E → F, if the norm has a local maximum at z, then the norm is constant in a neighborhood of z.

If the domain is a nontrivial finite dimensional space, then this implies the following version of the maximum modulus principle, see complex.exists_mem_frontier_is_max_on_norm. If f : E → F is complex differentiable on a nonempty compact set K, then there exists a point z ∈ frontier K such that λ z, ∥f z∥ takes it maximum value on K at z.

Finally, if the codomain is a strictly convex space, then the function cannot have a local maximum of the norm unless the function (not only its norm) is a constant. This version is not formalized yet.

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 only "public API" lemmas in this section are TODO and complex.norm_eq_norm_of_is_max_on_of_closed_ball_subset.

theorem complex.norm_max_aux₁ {F : Type v} [normed_group F] [normed_space F] [complete_space F] {f : → F} {z w : } (hd : diff_cont_on_cl f (metric.ball z (has_dist.dist w z))) (hz : is_max_on (has_norm.norm f) (metric.closed_ball z (has_dist.dist w z)) z) :

Now we drop the assumption complete_space F by embedding F into its completion.

theorem complex.norm_max_aux₂ {F : Type v} [normed_group F] [normed_space F] {f : → F} {z w : } (hd : diff_cont_on_cl f (metric.ball z (has_dist.dist w z))) (hz : is_max_on (has_norm.norm f) (metric.closed_ball z (has_dist.dist w z)) z) :

Then we replace the assumption is_max_on (norm ∘ f) (closed_ball z r) z with a seemingly weaker assumption is_max_on (norm ∘ f) (ball z r) z.

theorem complex.norm_max_aux₃ {F : Type v} [normed_group F] [normed_space F] {f : → F} {z w : } {r : } (hr : has_dist.dist w z = r) (hd : diff_cont_on_cl f (metric.ball z r)) (hz : is_max_on (has_norm.norm f) (metric.ball z r) z) :

Finally, we generalize the theorem from a disk in to a closed ball in any normed space.

theorem complex.norm_eq_on_closed_ball_of_is_max_on {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] {f : E → F} {z : E} {r : } (hd : diff_cont_on_cl f (metric.ball z r)) (hz : is_max_on (has_norm.norm f) (metric.ball z r) z) :

Maximum modulus principle on a closed ball: if f : E → F is continuous on a closed ball, is complex differentiable on the corresponding open ball, and the norm ∥f w∥ takes its maximum value on the open ball at its center, then the norm ∥f w∥ is constant on the closed ball.

Different forms of the maximum modulus principle #

theorem complex.norm_eq_norm_of_is_max_on_of_ball_subset {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] {f : E → F} {s : set E} {z w : E} (hd : diff_cont_on_cl f s) (hz : is_max_on (has_norm.norm f) s z) (hsub : metric.ball z (has_dist.dist w z) s) :

Maximum modulus principle: if f : E → F is complex differentiable on a set s, the norm of f takes it maximum on s at z and w is a point such that the closed ball with center z and radius dist w z is included in s, then ∥f w∥ = ∥f z∥.

theorem complex.norm_eventually_eq_of_is_local_max {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] {f : E → F} {c : E} (hd : ∀ᶠ (z : E) in nhds c, differentiable_at f z) (hc : is_local_max (has_norm.norm f) c) :
∀ᶠ (y : E) in nhds c, f y = f c

Maximum modulus principle: if f : E → F is complex differentiable in a neighborhood of c and the norm ∥f z∥ has a local maximum at c, then ∥f z∥ is locally constant in a neighborhood of c.

theorem complex.is_open_set_of_mem_nhds_and_is_max_on_norm {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] {f : E → F} {s : set E} (hd : differentiable_on f s) :
is_open {z : E | s nhds z is_max_on (has_norm.norm f) s z}
theorem complex.exists_mem_frontier_is_max_on_norm {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] [nontrivial E] [finite_dimensional E] {f : E → F} {U : set E} (hb : metric.bounded U) (hne : U.nonempty) (hd : diff_cont_on_cl f U) :
∃ (z : E) (H : z frontier U), is_max_on (has_norm.norm f) (closure U) z

Maximum modulus principle: if f : E → F is complex differentiable on a nonempty bounded set U and is continuous on its closure, then there exists a point z ∈ frontier U such that λ z, ∥f z∥ takes it maximum value on closure U at z.

theorem complex.norm_le_of_forall_mem_frontier_norm_le {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] [nontrivial E] {f : E → F} {U : set E} (hU : metric.bounded U) (hd : diff_cont_on_cl f U) {C : } (hC : ∀ (z : E), z frontier Uf z C) {z : E} (hz : z closure U) :
f z C

Maximum modulus principle: if f : E → F is complex differentiable on a bounded set U and ∥f z∥ ≤ C for any z ∈ frontier U, then the same is true for any z ∈ closure U.

theorem complex.eq_on_closure_of_eq_on_frontier {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] [nontrivial E] {f g : E → F} {U : set E} (hU : metric.bounded U) (hf : diff_cont_on_cl f U) (hg : diff_cont_on_cl g U) (hfg : set.eq_on f g (frontier U)) :

If two complex differentiable functions f g : E → F are equal on the boundary of a bounded set U, then they are equal on closure U.

theorem complex.eq_on_of_eq_on_frontier {E : Type u} [normed_group E] [normed_space E] {F : Type v} [normed_group F] [normed_space F] [nontrivial E] {f g : E → F} {U : set E} (hU : metric.bounded U) (hf : diff_cont_on_cl f U) (hg : diff_cont_on_cl g U) (hfg : set.eq_on f g (frontier U)) :
set.eq_on f g U

If two complex differentiable functions f g : E → F are equal on the boundary of a bounded set U, then they are equal on U.