English
Under the maximality condition on a ball, the norm at any interior point equals the norm at the center when passing to the closure via the limit arguments.
Русский
При условии максимума на шаре норма в точке внутри совпадает с нормой в центре после перехода к замыканию по пределам.
LaTeX
$$$$\\|f(w)\\| = \\|f(z)\\| \\quad\\text{for boundary points under the closure argument.}$$$$
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` and is
continuous on its closure. Suppose that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then
`f x = f c` for all `x ∈ closure U`. -/
theorem eqOn_closure_of_isPreconnected_of_isMaxOn_norm {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U)
(ho : IsOpen U) (hd : DiffContOnCl ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) :
EqOn f (const E (f c)) (closure U) :=
(eqOn_of_isPreconnected_of_isMaxOn_norm hc ho hd.differentiableOn hcU hm).of_subset_closure hd.continuousOn
continuousOn_const subset_closure Subset.rfl
