secant_mono_aux1 — Mathlib

English

If f is convex on s, then for x<y<z with x,z ∈ s the inequality (z−x) f(y) ≤ (z−y) f(x) + (y−x) f(z) holds.

Русский

Если f выпуклая на s, то для x<y<z и x,z ∈ s выполняется (z−x) f(y) ≤ (z−y) f(x) + (y−x) f(z).

LaTeX

$$$\text{ConvexOn } 𝕜\ s\ f \Rightarrow \forall x

Lean4

theorem secant_mono_aux1 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
    (z - x) * f y ≤ (z - y) * f x + (y - x) * f z :=
  by
  have hxy' : 0 < y - x := by linarith
  have hyz' : 0 < z - y := by linarith
  have hxz' : 0 < z - x := by linarith
  have ha : 0 ≤ (z - y) / (z - x) := by positivity
  have hb : 0 ≤ (y - x) / (z - x) := by positivity
  have key := hf.2 hx hz ha hb ?_
  · simp only [smul_eq_mul] at key
    ring_nf at key
    field_simp at key
    linear_combination key
  · field_simp
    ring

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