Working with convex functions

Stream: new members

[Leo Shine]

Hello I was trying to prove the theorem that convex functions on the real line were continuous, and I decided I needed this lemma below

before I did the epsilon delta arguments. In order to prove this I will need to expand out the convexity of g 4 times, with different parameters, but just doing it once seemed incredibly painful, and it seemed like just in order to prove that the arguments to it sum to one, I have to expand out 4 levels of Div.div, LinearOrderedField.toDiv... etc.

Presumably I'm doing something wrong here? Am I supposed to just prove that if something is convex on the reals that I can get the statements written out nicely directly? Or is there a nicer way of automatically unfolding everything so I can just use tactics like ring and field_simp?

import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Convex.Function
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.NNReal

lemma convexcontinuousineq (g:ℝ → ℝ ) (x:ℝ) (α :ℝ ) (hαpos : α >0) (hconv : ConvexOn ℝ Set.univ g) (hmid: g (x+α) = g (x - α))
  : ∀ y, |x- y| < α → g y ≤  g x + |x-y| * (g (x + α) - g x) / α ∧  g y ≥  g x - |x-y| * (g (x + α) - g x) / α
    := by
    intro y hy
    by_cases y ≤ x
    . constructor
      calc g y = g  (((α - |x-y|)/α  * x)  + (|x-y|/α) * (x - α)) := by ring; field_simp; rw[abs_of_nonneg]; ring; rw[mul_comm, ← mul_assoc]; field_simp; linarith
          _ ≤ (α - |x-y|) /(α)*  (g x) +  (|x-y|/α) * g (x-α)   := by
                                                                        apply hconv.2 _ _ _ _
                                                                        -- surely there's a nicer way to do this???
                                                                        unfold Div.div
                                                                        rw[LinearOrderedField.toDiv, Real.instLinearOrderedFieldReal]
                                                                        simp
                                                                        rw[DivInvMonoid.div', DivInvMonoid.div']
                                                                        ring_nf
                                                                        field_simp
                                                                        simp
                                                                        simp
                                                                        -- Seems like I'd need to do all that rewriting again????
                                                                        sorry
                                                                        sorry
          _ = g x + |x-y| * (g (x + α) - g x) / α := by sorry
      sorry
    sorry

[Ruben Van de Velde]

There should not be a Div.div in your goal state. I'm looking where it comes from...

[Eric Wieser]

Something seems to have gone wrong here; you shouldn't have ended up with Div.div in the goal in the first place

[Eric Wieser]

Here's a #mwe:

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Convex.Function

example (g : ℝ → ℝ ) (x y α : ℝ) (hconv : ConvexOn ℝ Set.univ g) (y : ℝ) :
    g (((α - |x-y|)/α * x) + (|x-y|/α) * (x - α)) ≤ (α - |x-y|)/α * g x + (|x-y|/α) * g (x-α) := by
  have := hconv.2 (Set.mem_univ x) (Set.mem_univ (x - α))
  apply this
  -- why do the goals contain `Div.div`?

[Ruben Van de Velde]

simp_rw [← smul_eq_mul]

before the apply fixes the issue

[Ruben Van de Velde]

import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Convex.Function
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.NNReal

lemma convexcontinuousineq (g:ℝ → ℝ ) (x:ℝ) (α :ℝ ) (hαpos : α >0) (hconv : ConvexOn ℝ Set.univ g) (hmid: g (x+α) = g (x - α))
  : ∀ y, |x- y| < α → g y ≤  g x + |x-y| * (g (x + α) - g x) / α ∧  g y ≥  g x - |x-y| * (g (x + α) - g x) / α
    := by
    intro y hy
    by_cases y ≤ x
    . constructor
      calc g y = g  (((α - |x-y|)/α  * x)  + (|x-y|/α) * (x - α)) := by ring; field_simp; rw[abs_of_nonneg]; ring; rw[mul_comm, ← mul_assoc]; field_simp; linarith
          _ ≤ (α - |x-y|) /(α)*  (g x) +  (|x-y|/α) * g (x-α)   := by
            simp_rw [← smul_eq_mul]
            apply hconv.2 (Set.mem_univ x) (Set.mem_univ (x - α)) _ _
            · ring_nf
              field_simp
            · apply div_nonneg ?_ hαpos.le
              rw [sub_nonneg]
              exact hy.le
            · apply div_nonneg ?_ hαpos.le
              exact abs_nonneg (x - y)
          _ = g x + |x-y| * (g (x + α) - g x) / α := by sorry
      sorry
    sorry

[Yaël Dillies]

Just FYI I have started the general argument here: !3#17081. You might also be inspired by @Malo Jaffré's proof: https://github.com/leanprover-community/mathlib/compare/convex-continuous

[Ruben Van de Velde]

(How many mathlib3 PRs of yours are gathering dust at this point?)

[Yaël Dillies]

~30. I am slowly but surely moving them to LeanCamCombi.

[Eric Wieser]

(possibly forever now that bors is dead on mathlib3 too)

[Leo Shine]

Thanks everyone, what was my mistake? Should I have started by using the \smul operation in the statement instead so that I didn't end up in this situation?

[Leo Shine]

@Yaël Dillies Cool I'll have a look

[Ruben Van de Velde]

The issue was using a lemma that's written in terms of smul and using it on a goal that uses *, which shouldn't really work but worked almost but not quite well enough here :)