English
Reiterates the norm equality under the completion and differentiability hypotheses for boundary behavior of holomorphic-like maps.
Русский
Повторение равенства норм под условия дополнения и дифференцируемости на границе для гомоморфных карт.
LaTeX
$$$$\\|f(w)\\| = \\|f(z)\\| \\quad\\text{under the same hypotheses as II with completion.}$$$$
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 z‖` is locally constant in a neighborhood
of `c`. -/
theorem norm_eventually_eq_of_isLocalMax {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₀,
norm_eqOn_closedBall_of_isMaxOn
(DifferentiableOn.diffContOnCl fun x hx => (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt)
fun x hx => (hr <| ball_subset_closedBall hx).2⟩
