noncomputable def cubicRegularizationLocalOptimalityMeasure {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (L M : ℝ) (x : E) : ℝ

Definition 4.1.4: the local optimality measure μ_M(x) for cubic regularization is the maximum of the square root of the scaled gradient norm term and the scaled negative least Hessian eigenvalue term.

def CubicRegularizationLocalOptimalityMeasure.«termμ[_;_;_](_)» : Lean.ParserDescr

@[simp]

theorem cubicRegularizationLocalOptimalityMeasure_eq_max {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (L M : ℝ) (x : E) : cubicRegularizationLocalOptimalityMeasure f L M x = max (√(2 / (L + M) * ‖gradient f x‖)) (-(2 / (2 * L + M)) * sInf (spectrum ℝ (hessian f x)))

The local optimality measure μ[f; L; M](x) is given by the textbook maximum formula.

theorem sqrt_scaledGradientNorm_le_cubicRegularizationLocalOptimalityMeasure {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (L M : ℝ) (x : E) : √(2 / (L + M) * ‖gradient f x‖) ≤ cubicRegularizationLocalOptimalityMeasure f L M x

The scaled gradient term is bounded above by the local optimality measure.

theorem scaledNegLeastHessianEigenvalue_le_cubicRegularizationLocalOptimalityMeasure {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (L M : ℝ) (x : E) : -(2 / (2 * L + M)) * sInf (spectrum ℝ (hessian f x)) ≤ cubicRegularizationLocalOptimalityMeasure f L M x

The scaled negative least-Hessian-eigenvalue term is bounded above by the local optimality measure.