continuous_on_of_convex_on_open

Stream: new members

[Malo Jaffré]

I've started working on proving that a convex function is continuous (if the domain is open):

Here is my work so far:

import analysis.convex.basic

lemma convex_on.slope_mono_adjacent {s : set ℝ} {f : ℝ → ℝ}
  {x y z: ℝ} (hx: x ∈ s) (hz: z ∈ s) (hxy: x < y) (hyz: y < z) (hf: convex_on s f) :
    (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) :=
begin
  have h₁: 0 < y - x := by linarith,
  have h₂: 0 < z - y := by linarith,
  have h₃: 0 < z - x := by linarith,

  suffices: f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y),
    begin ring at this ⊢, linarith end,

  set a := (z - y) / (z - x),
  set b := (y - x) / (z - x),

  have h₄: a + b = 1 :=
    begin field_simp, rw div_eq_iff; [ring, linarith] end,
  have h₅: a • x + b • z = y :=
    begin field_simp, rw div_eq_iff; [ring, linarith] end,

  have key :=
    hf.2 hx hz (show 0 ≤ a, by apply div_nonneg; linarith) (show 0 ≤ b, by apply div_nonneg; linarith) h₄,
  rw h₅ at key,
  replace key := mul_le_mul_of_nonneg_left key (le_of_lt h₃),

  field_simp [ne_of_gt h₁, ne_of_gt h₂, ne_of_gt h₃, mul_comm (z - x) _] at key ⊢,
  rw div_le_div_right; nlinarith,
end

Is this a good start to prove that for a convex function from R to R?

[Kevin Buzzard]

I don't know anything about convex functions but that's pretty neat Lean code. You've made clever use of the resources we have -- it's a bit of an arcane art using them.

[Malo Jaffré]

Thanks, I'll PR this then!

[Frédéric Dupuis]

This one is already in mathlib as it turns out: convex_on_real_of_slope_mono_adjacent in analysis/convex/basic.lean. But I don't think that the main result you're after is there -- that would indeed be a great addition!

[Malo Jaffré]

I think convex_on_real_of_slope_mono_adjacent is in the other direction though.

[Malo Jaffré]

#4307

[Frédéric Dupuis]

Oh, right -- I misread that mathlib lemma!

[Patrick Massot]

Malo, the PR process will be a lot easier for everyone if you have at look at https://leanprover-community.github.io/contribute/style.html#tactic-mode now. Coding syle conventions are mostly arbitrary, but uniformity really helps readers.

[Malo Jaffré]

Can I please get an invite to mathlib to continue working on this?

[Heather Macbeth]

@Malo Jaffré I think I did this!

[Malo Jaffré]

Thanks @Heather Macbeth, it worked!