English
If f is differentiable nearby c and has a local maximum of ||f|| at c, then there exists a neighborhood of c on which ||f|| is constant and equal to ||f(c)||.
Русский
Если f дифференцируема около c и ||f|| достигает локального максимума в c, то существует окрестность c, на которой ||f|| константа и равна ||f(c)||.
LaTeX
$$$$\\exists U\\ni c,\\ U\\text{ open},\\ \\forall x \\in U:\\ \\|f(x)\\| = \\|f(c)\\|.$$$$
Lean4
/-- **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 norm_eq_norm_of_isMaxOn_of_ball_subset {f : E → F} {s : Set E} {z w : E} (hd : DiffContOnCl ℂ f s)
(hz : IsMaxOn (norm ∘ f) s z) (hsub : ball z (dist w z) ⊆ s) : ‖f w‖ = ‖f z‖ :=
norm_eqOn_closedBall_of_isMaxOn (hd.mono hsub) (hz.on_subset hsub) (mem_closedBall.2 le_rfl)
