slope_strict_mono_adjacent — Mathlib

English

If f is strictly convex on s, then for any x < y < z with x, z ∈ s, the slope of the secant line on [x, y] is strictly less than the slope on [y, z].

Русский

Пусть f строго выпукла на s. Тогда для любых x < y < z с x, z ∈ s наклон секущей на [x, y] строго меньше наклона на [y, z].

LaTeX

$$$\text{StrictConvexOn } 𝕜\ s\ f \Rightarrow \forall x,y,z\in 𝕜,\ x∈s,\ z∈s,\ x

Lean4

/-- If `f : 𝕜 → 𝕜` is strictly convex, then for any three points `x < y < z` the slope of the
secant line of `f` on `[x, y]` is strictly less than the slope of the secant line of `f` on
`[y, z]`. -/
theorem slope_strict_mono_adjacent (hf : StrictConvexOn 𝕜 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
  have hxz' := hxz.ne
  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 hxz' ha hb (by field_simp; ring)
  simp only [smul_eq_mul] at key
  ring_nf at key
  field_simp at key ⊢
  linarith

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