noncomputable def cbpg_quadratic_gap_constant {p : ℕ} [Nonempty (Fin p)] (Lf : NNReal) (Li : Fin p → ↑PosReal) (R : ↑PosReal) : ℝ

The coefficient L_min / (2 p (L_f + L_max)^2 R^2) from Lemma 11.6, using the Chapter 11 owners cbpg_min_block_stepsize Li and cbpg_max_block_stepsize Li of the finite block extrema.

@[simp]

theorem cbpg_quadratic_gap_constant_def {p : ℕ} [Nonempty (Fin p)] (Lf : NNReal) (Li : Fin p → ↑PosReal) (R : ↑PosReal) : cbpg_quadratic_gap_constant Lf Li R = ↑(cbpg_min_block_stepsize Li) / (2 * ↑p * (↑Lf + ↑(cbpg_max_block_stepsize Li)) ^ 2 * ↑R ^ 2)

Expanding cbpg_quadratic_gap_constant yields the textbook coefficient L_min / (2 p (L_f + L_max)^2 R^2) with L_min = cbpg_min_block_stepsize Li and L_max = cbpg_max_block_stepsize Li.

def cbpgObjectiveGapSqBound {p : ℕ} [Nonempty (Fin p)] {X : Type u} [NormedAddCommGroup X] (Lf : NNReal) (Li : Fin p → ↑PosReal) (Rα : ↑PosReal) (F : X → EReal) (x : ℕ → X) (FOpt : ℝ) (k : ℕ) : Prop

The source quadratic gap estimate (11.18) used in Lemma 11.6.

def cbpgStepDecreaseBound {p : ℕ} [Nonempty (Fin p)] {X : Type u} [NormedAddCommGroup X] (Li : Fin p → ↑PosReal) (F : X → EReal) (x : ℕ → X) (k : ℕ) : Prop

The source sufficient-decrease estimate (11.11) used in Lemma 11.6.

theorem cbpg_step_decrease_ge_sq_objective_gap {p : ℕ} [Nonempty (Fin p)] {X : Type u} [NormedAddCommGroup X] {Lf : NNReal} {Li : Fin p → ↑PosReal} {F : X → EReal} {x : ℕ → X} {FOpt : ℝ} (Rα : ↑PosReal) (k : ℕ) (hGapSq : cbpgObjectiveGapSqBound Lf Li Rα F x FOpt k) (hStep : cbpgStepDecreaseBound Li F x k) : F (x k) - F (x (k + 1)) ≥ ↑(cbpg_quadratic_gap_constant Lf Li Rα * ((F (x (k + 1))).toReal - FOpt) ^ 2)

Lemma 11.6: abstracting the convex-CBPG proof to its two source inequalities, the quadratic objective-gap control (11.18) together with the sufficient-decrease estimate (11.11) implies the one-step lower bound F(xᵏ) - F(xᵏ⁺¹) ≥ c * (F(xᵏ⁺¹) - F_opt)^2, where c = L_min / (2 p (L_f + L_max)^2 R_α^2).