English
There exists a frontier point achieving the maximum of the norm on the closure of a bounded set under suitable differentiability assumptions.
Русский
Существуют frontier точки, где достигается максимум нормы на замыкании ограниченного множества при подходящих условиях дифференцируемости.
LaTeX
$$$$\\exists z \\in \\mathrm{frontier}(U), \\ IsMaxOn (\\|f\\|) (\\overline{U}) z.$$$$
Lean4
/-- If `f` is a function differentiable on the open unit ball, and there exists an `r < 1` such that
any value of `‖f‖` on the open ball is bounded above by some value on the closed ball of radius `r`,
then `f` is constant. -/
theorem eq_const_of_exists_le [ProperSpace E] {f : E → F} {r b : ℝ} (h_an : DifferentiableOn ℂ f (ball 0 b))
(hr_nn : 0 ≤ r) (hr_lt : r < b) (hr : ∀ z, z ∈ (ball 0 b) → ∃ w, w ∈ closedBall 0 r ∧ ‖f z‖ ≤ ‖f w‖) :
Set.EqOn f (Function.const E (f 0)) (ball 0 b) :=
by
obtain ⟨x, hx_mem, hx_max⟩ :=
isCompact_closedBall (0 : E) r |>.exists_isMaxOn (nonempty_closedBall.mpr hr_nn)
(h_an.continuousOn.mono <| closedBall_subset_ball hr_lt).norm
suffices Set.EqOn f (Function.const E (f x)) (ball 0 b) by rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]
apply eq_const_of_exists_max h_an (closedBall_subset_ball hr_lt hx_mem) (fun z hz ↦ ?_)
obtain ⟨w, hw, hw'⟩ := hr z hz
exact hw'.trans (hx_max hw)
