of_isLocalMin_of_convex_univ — Mathlib

English

If a local minimum on univ and convexity on univ hold, then the global minimum property holds for all points.

Русский

Если локальный минимум на всём множестве и выпуклость на всём множестве, то существует глобальный минимум на всём множестве.

LaTeX

$$$$ IsLocalMin f a \to ConvexOn \mathbb{R} \text{ on } \text{univ} f \to ∀ x, f(a) \le f(x). $$$$

Lean4

/-- A local minimum of a convex function is a global minimum. -/
theorem of_isLocalMin_of_convex_univ {f : E → β} {a : E} (h_local_min : IsLocalMin f a) (h_conv : ConvexOn ℝ univ f) :
    ∀ x, f a ≤ f x := fun x =>
  (IsMinOn.of_isLocalMinOn_of_convexOn (mem_univ a) (h_local_min.on univ) h_conv) (mem_univ x)

Похожие утверждения