English
If U is bounded, nonempty, and f is differentiable on U with a bounded-Abel-like maximal point on closure(U), then there exists a frontier point where the maximum is achieved.
Русский
Если U ограничено и непусто, а f дифференцируема на U и существует точка на границе, где ||f|| достигает максимума на closure(U), то такая точка лежит на frontier(U).
LaTeX
$$$$\\exists z \\in \\mathrm{frontier}(U),\\ IsMaxOn (\\|f\\|) (\\overline{U}) z.$$$$
Lean4
/-- **Maximum modulus principle**. Let `f : E → F` be a function between complex normed spaces.
Suppose that the codomain `F` is a strictly convex space, `f` is complex differentiable on a set
`s`, `f` is continuous on the closure of `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 eq_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 :=
have H₁ : ‖f w‖ = ‖f z‖ := norm_eq_norm_of_isMaxOn_of_ball_subset hd hz hsub
have H₂ : ‖f w + f z‖ = ‖f z + f z‖ := norm_eq_norm_of_isMaxOn_of_ball_subset (hd.add_const _) hz.norm_add_self hsub
eq_of_norm_eq_of_norm_add_eq H₁ <| by simp only [H₂, SameRay.rfl.norm_add, H₁]
