English
Given a real-valued function f on a proper space, if f is continuous on a closed ball and f has a strict inequality against the boundary, then there exists a point in the interior where f attains a local minimum.
Русский
Для функции f на правильном пространстве, если f непрерывна на замкнутом шаре и на границе выполняется строгое неравенство, то существует точка внутри шара, где f достигает локального минимума.
LaTeX
$$$\exists z \in B(a,r),\; IsLocalMin(f,z)$$$
Lean4
theorem exists_isLocalMin_mem_ball [TopologicalSpace β] [ConditionallyCompleteLinearOrder β] [OrderTopology β]
{f : α → β} {a z : α} {r : ℝ} (hf : ContinuousOn f (closedBall a r)) (hz : z ∈ closedBall a r)
(hf1 : ∀ z' ∈ sphere a r, f z < f z') : ∃ z ∈ ball a r, IsLocalMin f z :=
by
simp_rw [← closedBall_diff_ball] at hf1
exact (isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1 isOpen_ball
