Theorems · Theorem · complex analysis

Complex.eq_of_isMaxOn_of_ball_subset

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {s : Set E} {z w : E},
  DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → 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.

Defined in

Mathlib.Analysis.Complex.AbsMax

Cited by

1 results in Mathlib

Foundations

Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceStrictConvexSpace