secant_strict_mono_aux1 — Mathlib

English

If f is strictly convex on s, then for all x < y < z in s the slopes satisfy

Русский

Если f строго выпукла, то для x<y<z наклоны секущих удовлетворяют строгому неравенству:

LaTeX

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

Lean4

theorem secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 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 (by linarith) ha hb ?_
  · simp only [smul_eq_mul] at key
    ring_nf at key
    field_simp at key
    linear_combination key
  · field_simp
    ring

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