Convex implies monotone secants

Stream: Is there code for X?

[Heather Macbeth]

Do we have a lemma stating that if a function f : ℝ → ℝ is convex then the "secant based at x" function, sending y to (f y - f x) / (y - x), is monotone? Something like

example (hf : convex_on 𝕜 s f)
  {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : y ≠ x) (hyz : z ≠ x) (hyz : y < z) :
  (f y - f x) / (y - x) ≤ (f z - f x) / (z - x) :=

(maybe I need to be more careful about degenerate cases).

There are similar-looking lemmas like docs#convex_on.slope_mono_adjacent, but these are pickier about the relative order of the points.

[Kevin Buzzard]

(don't know the answer but probably you can have hyz : y \le z in the statement)

[David Loeffler]

I don't think so. The lemma docs#convex_on.slope_mono_adjacent is about pairs of secants that meet in the middle, while I think you're looking for a result about secants that meet at the ends, right?

[David Loeffler]

(there seems to be a typo in the docs, which is unhelpful)

[David Loeffler]

I bashed out a proof, shall I PR it to analysis.convex.slope?

[Heather Macbeth]

@David Loeffler Sure, thank you!

[Heather Macbeth]

I actually bashed out my own proof this afternoon too, feel free to mix and match any parts.

[Heather Macbeth]

lemma convex_on.secant_mono_aux1 (hf : convex_on 𝕜 s f)
  {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
  f y * (z - x) ≤ (z - y) * f x + (y - x) * f z :=
begin
  have hxy' : 0 < y - x := by linarith,
  have hyz' : 0 < z - y := by linarith,
  have hxz' : 0 < z - x := by linarith,
  rw ← le_div_iff hxz',
  have ha : 0 ≤ (z - y) / (z - x) := by positivity,
  have hb : 0 ≤ (y - x) / (z - x) := by positivity,
  calc _ = _ : _
  ... ≤ _ : hf.2 hx hz ha hb _
  ... = _ : _,
  { congr' 1,
    field_simp [hxy'.ne', hyz'.ne', hxz'.ne'],
    ring },
  { field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] },
  { field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] }
end

lemma convex_on.secant_mono_aux2 (hf : convex_on 𝕜 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 x) / (z - x) :=
begin
  have hxy' : 0 < y - x := by linarith,
  have hxz' : 0 < z - x := by linarith,
  rw div_le_div_iff hxy' hxz',
  linarith only [hf.secant_mono_aux1 hx hz hxy hyz],
end

lemma convex_on.secant_mono_aux3 (hf : convex_on 𝕜 s f)
  {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
  (f z - f x) / (z - x) ≤ (f z - f y) / (z - y) :=
begin
  have hyz' : 0 < z - y := by linarith,
  have hxz' : 0 < z - x := by linarith,
  rw div_le_div_iff hxz' hyz',
  linarith only [hf.secant_mono_aux1 hx hz hxy hyz],
end

lemma convex_on.secant_mono (hf : convex_on 𝕜 s f)
  {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x ≤ y) :
  (f x - f a) / (x - a) ≤ (f y - f a) / (y - a) :=
begin
  rcases eq_or_lt_of_le hxy with rfl | hxy,
  { simp },
  cases lt_or_gt_of_ne hxa with hxa hxa,
  { cases lt_or_gt_of_ne hya with hya hya,
    { convert hf.secant_mono_aux3 hx ha hxy hya using 1;
      rw ← neg_div_neg_eq;
      field_simp, },
    { convert hf.slope_mono_adjacent hx hy hxa hya using 1,
      rw ← neg_div_neg_eq;
      field_simp, } },
  { exact hf.secant_mono_aux2 ha hy hxa hxy, },
end

[David Loeffler]

Here's mine:

section slope_mono

variables {𝕜 : Type*} [linear_ordered_field 𝕜] {f : 𝕜 → 𝕜} {s : set 𝕜} {x x' y y' z : 𝕜}
  (hf : convex_on 𝕜 s f)
include hf

lemma slope_mono_right
 (hx : x ∈ s) (hy' : y' ∈ s) (hxy : x < y) (hyy' : y ≤ y') :
  (f y - f x) / (y - x) ≤ (f y' - f x) / (y' - x) :=
begin
  rw [div_le_div_iff (sub_pos.mpr hxy) (sub_pos.mpr (hxy.trans_le hyy')), ←sub_nonneg],
  have A : ((y' - y) / (y' - x)) • x  + ((y - x) / (y' - x)) • y' = y,
  { field_simp [(sub_pos.mpr (hxy.trans_le hyy')).ne'],
    ring },
  have B := hf.2 hx hy'
    (div_nonneg (sub_nonneg.mpr hyy') (sub_pos.mpr (hxy.trans_le hyy')).le)
    (div_pos (sub_pos.mpr hxy) (sub_pos.mpr (hxy.trans_le hyy'))).le
    (by field_simp [(sub_pos.mpr (hxy.trans_le hyy')).ne'] ),
  rw [A, smul_eq_mul, smul_eq_mul] at B,
  field_simp [(sub_pos.mpr (hxy.trans_le hyy')).ne'] at B,
  rw [le_div_iff (sub_pos.mpr (hxy.trans_le hyy')), ←sub_nonneg] at B,
  convert B using 1,
  ring,
end

lemma slope_mono_left (hx : x ∈ s) (hy : y ∈ s) (hxx' : x ≤ x') (hx'y : x' < y) :
  (f y - f x) / (y - x) ≤ (f y - f x') / (y - x') :=
begin
  rw [div_le_div_iff (sub_pos.mpr (hxx'.trans_lt hx'y)) (sub_pos.mpr hx'y), ←sub_nonneg],
  have A : ((y - x') / (y - x)) • x  + ((x' - x) / (y - x)) • y = x',
  { field_simp [(sub_pos.mpr (hxx'.trans_lt hx'y)).ne'],
    ring },
  have B := hf.2 hx hy
    (div_pos (sub_pos.mpr hx'y) (sub_pos.mpr (hxx'.trans_lt hx'y))).le
    (div_nonneg (sub_nonneg.mpr hxx') (sub_pos.mpr (hxx'.trans_lt hx'y)).le)
    (by field_simp [(sub_pos.mpr (hxx'.trans_lt hx'y)).ne'] ),
  rw [A, smul_eq_mul, smul_eq_mul] at B,
  field_simp [(sub_pos.mpr (hxx'.trans_lt hx'y)).ne'] at B,
  rw [le_div_iff (sub_pos.mpr (hxx'.trans_lt hx'y)), ←sub_nonneg] at B,
  convert B using 1,
  ring,
end

lemma slope_mono
  (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ s)
  (hxy : y ≠ x) (hxz : z ≠ x) (hyz : y ≤ z) :
  (f y - f x) / (y - x) ≤ (f z - f x) / (z - x) :=
begin
  rcases eq_or_lt_of_le hyz with rfl | hyz',
  { refl },
  rcases lt_or_lt_iff_ne.mpr hxy with hxy' | hxy',
  { rcases lt_or_lt_iff_ne.mpr hxz with hxz' | hxz',
    { -- y < z < x
      convert slope_mono_left hf hy hx hyz'.le hxz' using 1;
      { convert neg_div_neg_eq _ _, { ring }, { ring } } },
    { -- y < x < z
      convert convex_on.slope_mono_adjacent hf hy hz hxy' hxz' using 1;
      { convert neg_div_neg_eq _ _, { ring }, { ring } } } },
  { -- x < y ≤ z
    exact slope_mono_right hf hx hz hxy' hyz },
end

end slope_mono

[Heather Macbeth]

They look pretty similar, case bashing on the order of the three points involved.

[David Loeffler]

I think yours wins though -- there is too much duplication between slope_mono_left and slope_mono_right in mine.

[Heather Macbeth]

It's a bit surprising to me that nothing like this is there yet. Maybe it's because most of the convexity library is written in the multivariable/multidimensional setting?

[Heather Macbeth]

But I don't think there is any possible multivariable framing of this statement.

[Heather Macbeth]

Actually, our final lemmas are basically identical :-)

[Kevin Buzzard]

Great minds ;-)