English
If a complex-differentiable map on a connected domain has its modulus maximized at some point, then the map must be constant on the domain (assuming strict convexity of the target).
Русский
Если у комплексно дифференцируемого отображения на связной области модуль достигает максимума в точке, функция константна на всей области (при условии строгой выпуклости цели).
LaTeX
$$$( \max_{x \in U} \|f(x)\| = \|f(c)\| ) \Rightarrow \forall x \in U: f(x) = f(c)$$$
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 [StrictConvexSpace ℝ F] {f : M → F} {U : Set M} {c : M}
(hd : MDifferentiableOn I 𝓘(ℂ, F) f U) (hc : IsPreconnected U) (ho : IsOpen U) (hcU : c ∈ U)
(hm : IsMaxOn (norm ∘ f) U c) : EqOn f (const M (f c)) U := fun x hx =>
have H₁ : ‖f x‖ = ‖f c‖ := hd.norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hcU hm hx
have hd' : MDifferentiableOn I 𝓘(ℂ, F) (f · + f c) U := fun x hx ↦
⟨(hd x hx).1.add continuousWithinAt_const, (hd x hx).2.add_const _⟩
have H₂ : ‖f x + f c‖ = ‖f c + f c‖ := hd'.norm_eqOn_of_isPreconnected_of_isMaxOn hc ho 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]
