Coercivity Core Bound #
Proves that (1 - a)² * (V² + μ' * E²) ≤ 60 * Ln by resolving coupled
norm inequalities from the Nesterov accelerated gradient descent analysis.
theorem
PLAcceleratedNesterovLean.coercivity_core_bound
(T A U E D V s r a μ' Ln : ℝ)
(ha_nn : 0 ≤ a)
(ha_lt1 : a < 1)
(_hμ' : 0 < μ')
(hs_nn : 0 ≤ s)
(_hr_nn : 0 ≤ r)
(hs_sq : s ^ 2 = μ')
(hsr : s * r = a)
(hE_nn : 0 ≤ E)
(hU_nn : 0 ≤ U)
(hT_nn : 0 ≤ T)
(hA_nn : 0 ≤ A)
(hD_nn : 0 ≤ D)
(_hV_nn : 0 ≤ V)
(hT_le : T ^ 2 ≤ 2 * Ln)
(hU_le : U ^ 2 ≤ 2 * Ln)
(hD_le : μ' * D ^ 2 ≤ 2 * Ln)
(hv_orth : V ^ 2 = T ^ 2 + A ^ 2)
(hA_ub : A ≤ U + s * E)
(hE_ub : E ≤ D + r * V)
(hV_ub : V ≤ A + T)
: