English
If a function is differentiable near c and ||f|| has a local maximum at c, then the function is eventually constant in a neighborhood of c on the norm.
Русский
Если f дифференцируема около c и ||f|| имеет локальный максимум в c, то окрестность c отображает константность нормы.
LaTeX
$$$$\\forall \\, c, \\text{ if } hd \\text{ and } hc, \\ then \\ ∃ U \\ni c: \\forall x \\in U, \\|f(x)\\| = \\|f(c)\\|.$$$$
Lean4
/-- **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 eventually_eq_of_isLocalMax_norm {f : E → F} {c : E} (hd : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z)
(hc : IsLocalMax (norm ∘ f) c) : ∀ᶠ y in 𝓝 c, f y = f c :=
by
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
exact
nhds_basis_closedBall.eventually_iff.2
⟨r, hr₀,
eqOn_closedBall_of_isMaxOn_norm
(DifferentiableOn.diffContOnCl fun x hx => (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt)
fun x hx => (hr <| ball_subset_closedBall hx).2⟩
