(4.9), proof of Theorem 4.4, p. 307 — second term: η∇f(x_t)⊤(y_{t+1} − x_{t+1}) ≤ D_Φ(x_{t+1}, x_t) − (ρ/2)‖x_{t+1} − y_{t+1}‖² − (ρ/2)‖y_{t+1} − x_t‖²

import Mathlib
import Definitions.Def_ConvexOptAlg_MirrorProx_Defs

namespace ConvexOptAlg.MirrorProx

/-- The second term in the proof of Theorem 4.4 (Bubeck, arXiv:1405.4980v2, §4.5, p. 307, first
display, through (4.9)): for a run of mirror prox with step size `η`, a mirror map `Φ` that is
`ρ`-strongly convex on `X ∩ D`, and every `t ≥ 1`,
1. `η∇f(x_t)⊤(y_{t+1} − x_{t+1}) ≤ D_Φ(x_{t+1}, x_t) − D_Φ(x_{t+1}, y_{t+1}) − D_Φ(y_{t+1}, x_t)`
   (4.9);
2. `η∇f(x_t)⊤(y_{t+1} − x_{t+1})
     ≤ D_Φ(x_{t+1}, x_t) − (ρ/2)‖x_{t+1} − y_{t+1}‖² − (ρ/2)‖y_{t+1} − x_t‖²`. -/
theorem eq_4_9 {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 Φ Φ')
    (ρ : ℝ) (hsc : IsStronglyConvexWRT (X ∩ D) Φ Φ' ρ)
    (f' : E → E →L[ℝ] ℝ) (η : ℝ) (x y y' x' : ℕ → E)
    (hrun : IsMirrorProxRun X D Φ Φ' f' η x y y' x')
    (t : ℕ) (ht : 1 ≤ t) :
    η * f' (x t) (y (t + 1) - x (t + 1))
        ≤ bregman Φ Φ' (x (t + 1)) (x t) - bregman Φ Φ' (x (t + 1)) (y (t + 1))
            - bregman Φ Φ' (y (t + 1)) (x t) ∧
      η * f' (x t) (y (t + 1) - x (t + 1))
        ≤ bregman Φ Φ' (x (t + 1)) (x t) - ρ / 2 * ‖x (t + 1) - y (t + 1)‖ ^ 2
            - ρ / 2 * ‖y (t + 1) - x t‖ ^ 2 := by sorry

end ConvexOptAlg.MirrorProx