English
If a differentiable function on a ball attains its maximum of the norm at a point, then it is constant on the ball.
Русский
Если на шаре найдется точка, где достигается максимум нормы, функция постоянна на шаре.
LaTeX
$$$$\\text{If } \\text{hd is differentiable on ball}(0,b) \\text{ and } z \\text{ is a maximizer of } \\|f\\|, \\text{ then } f\\equiv f(z) \\text{ on } \\text{ball}(0,b).$$$$
Lean4
/-- **Maximum modulus principle** on a closed ball. Suppose that a function `f : E → F` from a
normed complex space to a strictly convex normed complex space has the following properties:
- it is continuous on a closed ball `Metric.closedBall z r`,
- it is complex differentiable on the corresponding open ball;
- the norm `‖f w‖` takes its maximum value on the open ball at its center.
Then `f` is a constant on the closed ball. -/
theorem eqOn_closedBall_of_isMaxOn_norm {f : E → F} {z : E} {r : ℝ} (hd : DiffContOnCl ℂ f (ball z r))
(hz : IsMaxOn (norm ∘ f) (ball z r) z) : EqOn f (const E (f z)) (closedBall z r) := fun _x hx =>
eq_of_isMaxOn_of_ball_subset hd hz <| ball_subset_ball hx
