min_le_of_mem_segment — Mathlib

English

For a concave function on a segment, the minimum on the segment occurs at an endpoint.

Русский

Для вогнутой функции на отрезке минимум достигается в концах отрезка.

LaTeX

$$$ \text{ConcaveOn}_{\mathbb{K}}(s,f) \Rightarrow \min_{z\in \text{segment}(x,y)} f(z) \text{ occurs at } x \text{ or } y$$$

Lean4

/-- **Minimum principle** for concave functions on a segment. If a function `f` is concave on the
segment `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`. -/
theorem min_le_of_mem_segment (hf : ConcaveOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) :
    min (f x) (f y) ≤ f z :=
  hf.dual.le_max_of_mem_segment hx hy hz

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