Documentation

Mathlib.Analysis.Complex.AbsMax

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.

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.

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.

theorem Complex.norm_max_aux₁ {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {f : F} {z : } {w : } (hd : DiffContOnCl f (Metric.ball z (dist w z))) (hz : IsMaxOn (norm f) (Metric.closedBall z (dist w z)) z) :

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

theorem Complex.norm_max_aux₂ {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : F} {z : } {w : } (hd : DiffContOnCl f (Metric.ball z (dist w z))) (hz : IsMaxOn (norm f) (Metric.closedBall z (dist w z)) z) :

Then we replace the assumption IsMaxOn (norm ∘ f) (Metric.closedBall z r) z with a seemingly weaker assumption IsMaxOn (norm ∘ f) (Metric.ball z r) z.

theorem Complex.norm_max_aux₃ {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : F} {z : } {w : } {r : } (hr : dist w z = r) (hd : DiffContOnCl f (Metric.ball z r)) (hz : IsMaxOn (norm f) (Metric.ball z r) z) :

Maximum modulus principle for any codomain #

If we do not assume that the codomain is a strictly convex space, then we can only claim that the norm ‖f x‖ is locally constant.

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

theorem Complex.norm_eqOn_closedBall_of_isMaxOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {z : E} {r : } (hd : DiffContOnCl f (Metric.ball z r)) (hz : IsMaxOn (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.

theorem Complex.norm_eq_norm_of_isMaxOn_of_ball_subset {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {s : Set E} {z : E} {w : E} (hd : DiffContOnCl f s) (hz : IsMaxOn (norm f) s z) (hsub : Metric.ball z (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_isLocalMax {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {c : E} (hd : ∀ᶠ (z : E) in nhds c, DifferentiableAt f z) (hc : IsLocalMax (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.isOpen_setOf_mem_nhds_and_isMaxOn_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {s : Set E} (hd : DifferentiableOn f s) :
IsOpen {z : E | s nhds z IsMaxOn (norm f) s z}
theorem Complex.norm_eqOn_of_isPreconnected_of_isMaxOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn f U) (hcU : c U) (hm : IsMaxOn (norm f) U c) :
Set.EqOn (norm f) (Function.const E f c) U

Maximum modulus principle on a connected set. Let U be a (pre)connected open set in a complex normed space. Let f : E → F be a function that is complex differentiable on U. Suppose that ‖f x‖ takes its maximum value on U at c ∈ U. Then ‖f x‖ = ‖f c‖ for all x ∈ U.

theorem Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] {f : EF} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DiffContOnCl f U) (hcU : c U) (hm : IsMaxOn (norm f) U c) :

Maximum modulus principle on a connected set. Let U be a (pre)connected open set in a complex normed space. Let f : E → F be a function that is complex differentiable on U and is continuous on its closure. Suppose that ‖f x‖ takes its maximum value on U at c ∈ U. Then ‖f x‖ = ‖f c‖ for all x ∈ closure U.

The case of a strictly convex codomain #

If the codomain F is a strictly convex space, then we can claim equalities like f w = f z instead of ‖f w‖ = ‖f z‖.

Instead of repeating the proof starting with lemmas about integrals, we apply a corresponding lemma above twice: for f and for (f · + f c). Then we have ‖f w‖ = ‖f z‖ and ‖f w + f z‖ = ‖f z + f z‖, thus ‖f w + f z‖ = ‖f w‖ + ‖f z‖. This is only possible if f w = f z, see eq_of_norm_eq_of_norm_add_eq.

theorem Complex.eqOn_of_isPreconnected_of_isMaxOn_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [StrictConvexSpace F] {f : EF} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn f U) (hcU : c U) (hm : IsMaxOn (norm f) U c) :
Set.EqOn f (Function.const E (f c)) U

Maximum modulus principle on a connected set. Let U be a (pre)connected open set in a complex normed space. Let f : E → F be a function that is complex differentiable on U. Suppose that ‖f x‖ takes its maximum value on U at c ∈ U. Then f x = f c for all x ∈ U.

TODO: change assumption from IsMaxOn to IsLocalMax.

theorem Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [StrictConvexSpace F] {f : EF} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DiffContOnCl f U) (hcU : c U) (hm : IsMaxOn (norm f) U c) :

Maximum modulus principle on a connected set. Let U be a (pre)connected open set in a complex normed space. Let f : E → F be a function that is complex differentiable on U and is continuous on its closure. Suppose that ‖f x‖ takes its maximum value on U at c ∈ U. Then f x = f c for all x ∈ closure U.

theorem Complex.eq_of_isMaxOn_of_ball_subset {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [StrictConvexSpace F] {f : EF} {s : Set E} {z : E} {w : E} (hd : DiffContOnCl f s) (hz : IsMaxOn (norm f) s z) (hsub : Metric.ball z (dist w z) s) :
f w = f z

Maximum modulus principle. Let f : E → F be a function between complex normed spaces. Suppose that the codomain F is a strictly convex space, f is complex differentiable on a set s, f is continuous on the closure of 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.eqOn_closedBall_of_isMaxOn_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [StrictConvexSpace F] {f : EF} {z : E} {r : } (hd : DiffContOnCl f (Metric.ball z r)) (hz : IsMaxOn (norm f) (Metric.ball z r) z) :

Maximum modulus principle on a closed ball. Suppose that a function f : E → F from a normed complex space to a strictly convex normed complex space has the following properties:

  • it is continuous on a closed ball Metric.closedBall z r,
  • it is complex differentiable on the corresponding open ball;
  • the norm ‖f w‖ takes its maximum value on the open ball at its center.

Then f is a constant on the closed ball.

theorem Complex.eventually_eq_of_isLocalMax_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [StrictConvexSpace F] {f : EF} {c : E} (hd : ∀ᶠ (z : E) in nhds c, DifferentiableAt f z) (hc : IsLocalMax (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 is locally constant in a neighborhood of c.

theorem Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : E} (hf : ∀ᶠ (z : E) in nhds c, DifferentiableAt f z) (hc : IsLocalMin (norm f) c) :
(∀ᶠ (z : E) in nhds c, f z = f c) f c = 0

Maximum on a set vs maximum on its frontier #

In this section we prove corollaries of the maximum modulus principle that relate the values of a function on a set to its values on the frontier of this set.

theorem Complex.exists_mem_frontier_isMaxOn_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [Nontrivial E] [FiniteDimensional E] {f : EF} {U : Set E} (hb : Bornology.IsBounded U) (hne : Set.Nonempty U) (hd : DiffContOnCl f U) :
∃ z ∈ frontier U, IsMaxOn (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 (‖f ·‖) takes it maximum value on closure U at z.

theorem Complex.norm_le_of_forall_mem_frontier_norm_le {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [Nontrivial E] {f : EF} {U : Set E} (hU : Bornology.IsBounded U) (hd : DiffContOnCl f U) {C : } (hC : zfrontier U, f 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.eqOn_closure_of_eqOn_frontier {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [Nontrivial E] {f : EF} {g : EF} {U : Set E} (hU : Bornology.IsBounded U) (hf : DiffContOnCl f U) (hg : DiffContOnCl g U) (hfg : Set.EqOn 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.eqOn_of_eqOn_frontier {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {F : Type v} [NormedAddCommGroup F] [NormedSpace F] [Nontrivial E] {f : EF} {g : EF} {U : Set E} (hU : Bornology.IsBounded U) (hf : DiffContOnCl f U) (hg : DiffContOnCl g U) (hfg : Set.EqOn f g (frontier U)) :
Set.EqOn 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.