English
If a differentiable function on a ball attains its maximum of the norm at some interior point, then the function is constant on the ball.
Русский
Если на шаре функция достигает максимума нормы в некоторой внутренней точке, то функция постоянна на шаре.
LaTeX
$$$$\\text{If } \\text{hd on ball}(0,b) \\text{ and } v\\in B(0,b) \\text{ with max, then } f\\equiv f(v) \\text{ on } B(0,b).$$$$
Lean4
/-- If `f` is differentiable on the open unit ball `{z : ℂ | ‖z‖ < 1}`, and `‖f‖` attains a maximum
in this open ball, then `f` is constant. -/
theorem eq_const_of_exists_max {f : E → F} {b : ℝ} (h_an : DifferentiableOn ℂ f (ball 0 b)) {v : E} (hv : v ∈ ball 0 b)
(hv_max : IsMaxOn (norm ∘ f) (ball 0 b) v) : Set.EqOn f (Function.const E (f v)) (ball 0 b) :=
Complex.eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball 0 b).isPreconnected isOpen_ball h_an hv hv_max
