slope_mono_adjacent — Mathlib

English

If f is convex on a set s and x < y < z are in s, then the slope on [x,y] is at most the slope on [y,z].

Русский

Если f выпукла на множестве s и x < y < z принадлежат s, то наклон секантной линии на [x,y] не превосходит наклон на [y,z].

LaTeX

$$$\\text{ConvexOn}(𝕜, s, f) \\Rightarrow \\text{for } x

Lean4

/-- If `f : 𝕜 → 𝕜` is convex, then for any three points `x < y < z` the slope of the secant line of
`f` on `[x, y]` is less than the slope of the secant line of `f` on `[y, z]`. -/
theorem slope_mono_adjacent (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
    (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) :=
  by
  have hxz := hxy.trans hyz
  rw [← sub_pos] at hxy hxz hyz
  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 (by field_simp; ring)
  simp only [smul_eq_mul] at key
  ring_nf at key
  field_simp at key ⊢
  linarith

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