§4.5, proof of Theorem 4.4, p. 307 — third term: (∇f(y_{t+1}) − ∇f(x_t))⊤(y_{t+1} − x_{t+1}) ≤ (β/2)‖y_{t+1} − x_t‖² + (β/2)‖y_{t+1} − x_{t+1}‖²

import Mathlib
import Definitions.Def_ConvexOptAlg_MirrorProx_Defs

namespace ConvexOptAlg.MirrorProx

/-- The third term in the proof of Theorem 4.4 (Bubeck, arXiv:1405.4980v2, §4.5, p. 307, second
display): for a run of mirror prox with step size `η` on a function `f` that is `β`-smooth on `X`
w.r.t. `‖·‖` (gradient map `f'`), and every `t ≥ 1`,
`(∇f(y_{t+1}) − ∇f(x_t))⊤(y_{t+1} − x_{t+1}) ≤ ‖∇f(y_{t+1}) − ∇f(x_t)‖∗ · ‖y_{t+1} − x_{t+1}‖`,
`‖∇f(y_{t+1}) − ∇f(x_t)‖∗ · ‖y_{t+1} − x_{t+1}‖ ≤ β‖y_{t+1} − x_t‖ · ‖y_{t+1} − x_{t+1}‖`, and
`β‖y_{t+1} − x_t‖ · ‖y_{t+1} − x_{t+1}‖ ≤ (β/2)‖y_{t+1} − x_t‖² + (β/2)‖y_{t+1} − x_{t+1}‖²`.
The dual norm `‖·‖∗` is the operator norm on `E →L[ℝ] ℝ`. -/
theorem thm_4_4_third_term {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    (X D : Set E) (hXc : IsCompact X) (hXconv : Convex ℝ X) (hXD : X ⊆ closure D)
    (hXDne : (X ∩ D).Nonempty)
    (Φ : E → ℝ) (Φ' : E → E →L[ℝ] ℝ) (hΦ : IsMirrorMap D Φ Φ')
    (f : E → ℝ) (f' : E → E →L[ℝ] ℝ) (β : ℝ) (hsm : IsSmoothWRT X f f' β)
    (η : ℝ) (x y y' x' : ℕ → E)
    (hrun : IsMirrorProxRun X D Φ Φ' f' η x y y' x')
    (t : ℕ) (ht : 1 ≤ t) :
    (f' (y (t + 1)) - f' (x t)) (y (t + 1) - x (t + 1))
        ≤ ‖f' (y (t + 1)) - f' (x t)‖ * ‖y (t + 1) - x (t + 1)‖ ∧
      ‖f' (y (t + 1)) - f' (x t)‖ * ‖y (t + 1) - x (t + 1)‖
        ≤ β * ‖y (t + 1) - x t‖ * ‖y (t + 1) - x (t + 1)‖ ∧
      β * ‖y (t + 1) - x t‖ * ‖y (t + 1) - x (t + 1)‖
        ≤ β / 2 * ‖y (t + 1) - x t‖ ^ 2 + β / 2 * ‖y (t + 1) - x (t + 1)‖ ^ 2 := by sorry

end ConvexOptAlg.MirrorProx