English
If dist(w,z) = r and f is differentiable on ball, and z is a maximum point, then the boundary behavior forces equality of norms at w and z.
Русский
Если dist(w,z) = r и f дифференцируема на шаре, а z является максимумом, то на границе поведение заставляет равенство норм в w и z.
LaTeX
$$$$\\forall f, z, w, r,\\ hd, hz: \\|f(w)\\| = \\|f(z)\\|.$$$$
Lean4
theorem norm_max_aux₃ {f : ℂ → F} {z w : ℂ} {r : ℝ} (hr : dist w z = r) (hd : DiffContOnCl ℂ f (ball z r))
(hz : IsMaxOn (norm ∘ f) (ball z r) z) : ‖f w‖ = ‖f z‖ :=
by
subst r
rcases eq_or_ne w z with (rfl | hne); · rfl
rw [← dist_ne_zero] at hne
exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)
