English
Let U be a connected open set in a complex normed space, f differentiable on U, and continuous on closure(U). If ||f|| attains its maximum at some c in U, then f is constant on closure(U).
Русский
Пусть U — связанное открытое множество в комплексном нормированном пространстве, f дифференцируема на U и непрерывна на замыкании. Если ||f|| достигает максимума в U в точке c, то f постоянна на closure(U).
LaTeX
$$$$\\text{If } f \\text{ is differentiable on } U,\\ f \\text{ continuous on } \\overline{U},\\ and\\ \\|f(x)\\| \\le \\|f(c)\\| \\text{ for all } x \\in U, \\text{ then } f\\equiv f(c) \\text{ on } \\overline{U}.$$$$
Lean4
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space. Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then `f x = f c` for all `x ∈ U`.
TODO: change assumption from `IsMaxOn` to `IsLocalMax`. -/
theorem eqOn_of_isPreconnected_of_isMaxOn_norm {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U)
(hd : DifferentiableOn ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : EqOn f (const E (f c)) U := fun x hx =>
have H₁ : ‖f x‖ = ‖f c‖ := norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hd hcU hm hx
have H₂ : ‖f x + f c‖ = ‖f c + f c‖ :=
norm_eqOn_of_isPreconnected_of_isMaxOn hc ho (hd.add_const _) hcU hm.norm_add_self hx
eq_of_norm_eq_of_norm_add_eq H₁ <| by simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]
