theorem barrier_parameter_bound_iff_gradient_inner_sq_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {F : E → ℝ} {ν : NNReal} {x : E} (hPos : (hessian F x).IsPositive) : (∀ (u : E), 2 * inner ℝ (gradient F x) u - inner ℝ u ((hessian F x) u) ≤ ↑ν) ↔ ∀ (u : E), inner ℝ (gradient F x) u ^ 2 ≤ ↑ν * hessianLocalNorm F x u ^ 2

Proposition 5.3.3, pointwise owner form: at a fixed point x with positive Hessian, the barrier inequality 2 ⟪∇ F(x), u⟫ - ⟪∇² F(x)u, u⟫ ≤ ν for every direction u is equivalent to the quadratic-form bound ⟪∇ F(x), u⟫² ≤ ν ‖u‖[F; x]^2 for every u, written on the canonical Chapter 5 local-norm surface.