English
If f is complex differentiable near z and achieves a local maximum of the norm at z, then the norm is locally constant near z.
Русский
Если f дифференцируема в окрестности z и достигает локального максимума нормы в z, то норма константа в окрестности z.
LaTeX
$$$$\\forall f,z: \\text{if } \\exists \\text{ neighborhood where } \\|f\\| \\text{ has a local maximum at } z, \\text{ then } \\|f\\| \\text{ is locally constant near } z.$$$$
Lean4
/-- **Maximum modulus principle** on a closed ball: if `f : E → F` is continuous on a closed ball,
is complex differentiable on the corresponding open ball, and the norm `‖f w‖` takes its maximum
value on the open ball at its center, then the norm `‖f w‖` is constant on the closed ball. -/
theorem norm_eqOn_closedBall_of_isMaxOn {f : E → F} {z : E} {r : ℝ} (hd : DiffContOnCl ℂ f (ball z r))
(hz : IsMaxOn (norm ∘ f) (ball z r) z) : EqOn (norm ∘ f) (const E ‖f z‖) (closedBall z r) :=
by
intro w hw
rw [mem_closedBall, dist_comm] at hw
rcases eq_or_ne z w with (rfl | hne); · rfl
set e := (lineMap z w : ℂ → E)
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa [e]
have hr : dist (1 : ℂ) 0 = 1 := by simp
have hball : MapsTo e (ball 0 1) (ball z r) :=
by
refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono Subset.rfl ?_
simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw
exact norm_max_aux₃ hr (hd.comp hde.diffContOnCl hball) (hz.comp_mapsTo hball (lineMap_apply_zero z w))
