English
Under strict convexity, a holomorphic map with maximal modulus at a point on a connected open set must be constant.
Русский
При строгой выпуклости модуля у голоморфной отображения на связном открытом множестве максимум модуля в точке приводит к константности отображения.
LaTeX
$$$\forall x \in U:\ f(x) = f(c)$$$
Lean4
/-- If a function `f : M → F` from a complex manifold to a complex normed space is holomorphic on a
(pre)connected compact open set, then it is a constant on this set. -/
theorem apply_eq_of_isPreconnected_isCompact_isOpen {f : M → F} {U : Set M} {a b : M}
(hd : MDifferentiableOn I 𝓘(ℂ, F) f U) (hpc : IsPreconnected U) (hc : IsCompact U) (ho : IsOpen U) (ha : a ∈ U)
(hb : b ∈ U) : f a = f b :=
by
refine
?_
-- Subtract `f b` to avoid the assumption `[StrictConvexSpace ℝ F]`
wlog hb₀ : f b = 0 generalizing f
· have hd' : MDifferentiableOn I 𝓘(ℂ, F) (f · - f b) U := fun x hx ↦
⟨(hd x hx).1.sub continuousWithinAt_const, (hd x hx).2.sub_const _⟩
simpa [sub_eq_zero] using this hd' (sub_self _)
rcases hc.exists_isMaxOn ⟨a, ha⟩ hd.continuousOn.norm with ⟨c, hcU, hc⟩
have : ∀ x ∈ U, ‖f x‖ = ‖f c‖ := norm_eqOn_of_isPreconnected_of_isMaxOn hd hpc ho hcU hc
rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
