theorem gradientMapping_minimizes_objective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {Q : Set E} (hQ_nonempty : Q.Nonempty) (hQ_closed : IsClosed Q) (hQ_convex : Convex ℝ Q) {f : E → ℝ} {xBar : E} {γ : NNRealˣ} : gradientMapping Q hQ_nonempty hQ_closed hQ_convex f xBar γ ∈ Q ∧ IsMinOn (quadraticallyRegularizedObjective (firstOrderTaylorModelAt f xBar) (↑↑γ) xBar) Q (gradientMapping Q hQ_nonempty hQ_closed hQ_convex f xBar γ)

The projected-gradient point belongs to Q and minimizes the quadratically regularized first-order Taylor model from Definition 2.35 over Q.