Theorems · Theorem · complex analysis

Complex.norm_eqOn_closedBall_of_isMaxOn

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {z : E} {r : ℝ},
  DiffContOnCl ℂ f (Metric.ball z r) →
    IsMaxOn (norm ∘ f) (Metric.ball z r) z → Set.EqOn (norm ∘ f) (Function.const E ‖f z‖) (Metric.closedBall z r)

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.

Defined in

Mathlib.Analysis.Complex.AbsMax

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace