English
Let U be a connected open set, and f differentiable in the complex sense on U. If the modulus of f attains a maximum at c in U, then |f| is constant on U and equals |f(c)|.
Русский
Пусть U — связное открытое множество, и f дифференцируема по комплексному направлению на U. Если модуль f достигает на U максимума в точке c, то модуль f постоянен на U и равен |f(c)|.
LaTeX
$$$\bigl( \max_{x \in U} \|f(x)\| = \|f(c)\| \bigr) \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`. -/
theorem norm_eqOn_of_isPreconnected_of_isMaxOn {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 (norm ∘ f) (const M ‖f c‖) U := by
set V := {z ∈ U | ‖f z‖ = ‖f c‖}
suffices U ⊆ V from fun x hx ↦ (this hx).2
have hVo : IsOpen V := by
refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_
replace hm : IsLocalMax (‖f ·‖) x := mem_of_superset (ho.mem_nhds hx.1) fun z hz ↦ (hm hz).out.trans_eq hx.2.symm
replace hd : ∀ᶠ y in 𝓝 x, MDifferentiableAt I 𝓘(ℂ, F) f y :=
(eventually_mem_nhds_iff.2 (ho.mem_nhds hx.1)).mono fun z ↦ hd.mdifferentiableAt
exact (Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦ (Eq.trans · hx.2)
have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, rfl⟩
set W := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
have hdVW : Disjoint V W := disjoint_compl_right.mono inf_le_right inf_le_right
have hUVW : U ⊆ V ∪ W := fun x hx => (eq_or_ne ‖f x‖ ‖f c‖).imp (.intro hx) (.intro hx)
exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne
