theorem regularizedModelValue_mu_ge_L_sub_sq_norm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {μ : ℝ} {L : NNReal} {f : E → ℝ} (hf : f ∈ setOf (IsStrongConvexSmoothObjective μ ↑L)) (t : ℝ) (xBar xL : E) (hxL : IsMinOn (quadraticallyRegularizedObjective f (↑L) xBar) Set.univ xL) : have gL := reducedGradientOf (↑L) xBar xL; (fun (t : ℝ) (xBar : E) (γ : ℝ) => ((fun (t : ℝ) (xBar : E) (γ : ℝ) => (SetConstrainedMinimizationProblem.unconstrained (quadraticallyRegularizedObjective ((fun (t : ℝ) (x : E) => f x - t) t) γ xBar)).optimalValue) t xBar γ).toReal) t xBar μ ≥ (fun (t : ℝ) (xBar : E) (γ : ℝ) => ((fun (t : ℝ) (xBar : E) (γ : ℝ) => (SetConstrainedMinimizationProblem.unconstrained (quadraticallyRegularizedObjective ((fun (t : ℝ) (x : E) => f x - t) t) γ xBar)).optimalValue) t xBar γ).toReal) t xBar ↑L - (↑L - μ) / (2 * μ * ↑L) * ‖gL‖ ^ 2

Proposition 2.27: if xL minimizes the unshifted regularized objective x ↦ f x + (L / 2) ‖x - xBar‖² and gL := reducedGradientOf (L : ℝ) xBar xL, then the shifted exact regularized values satisfy f^*(t; xBar; μ) ≥ f^*(t; xBar; L) - ((L - μ) / (2 μ L)) ‖gL‖². The textbook ℝⁿ statement is recovered by specializing E := EuclideanSpace ℝ (Fin n).