Algebraic helper lemmas for the flat-case Lyapunov bound

Provides norm expansions, Pythagorean decompositions, inner product decompositions, and cross-term vanishing for orthogonal projectors.

Orthogonality from self-adjoint + idempotent

theorem PLAcceleratedNesterovLean.proj_orth_inner {d : ℕ} (P : E d →L[ℝ] E d) (hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_idem : ∀ (x : E d), P (P x) = P x) (v : E d) : inner ℝ (P v) (v - P v) = 0

Pythagorean decomposition

theorem PLAcceleratedNesterovLean.pythagorean_proj {d : ℕ} (P : E d →L[ℝ] E d) (hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_idem : ∀ (x : E d), P (P x) = P x) (v : E d) : ‖v‖ ^ 2 = ‖P v‖ ^ 2 + ‖v - P v‖ ^ 2

Cross-term vanishing

theorem PLAcceleratedNesterovLean.cross_term_Pg_b {d : ℕ} (P : E d →L[ℝ] E d) (hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_idem : ∀ (x : E d), P (P x) = P x) (g v : E d) : inner ℝ (P g) (v - P v) = 0

theorem PLAcceleratedNesterovLean.cross_term_Pperpg_Pv {d : ℕ} (P : E d →L[ℝ] E d) (hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_idem : ∀ (x : E d), P (P x) = P x) (g v : E d) : inner ℝ (g - P g) (P v) = 0

Inner product decomposition

theorem PLAcceleratedNesterovLean.inner_proj_decomp {d : ℕ} (P : E d →L[ℝ] E d) (hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_idem : ∀ (x : E d), P (P x) = P x) (g v : E d) : inner ℝ g v = inner ℝ (P g) (P v) + inner ℝ (g - P g) (v - P v)

Norm of wn = (1-a)•b + √μ'•en - √η•P⊥g

theorem PLAcceleratedNesterovLean.norm_three_term_sq {d : ℕ} (b en ppg : E d) (c1 c2 c3 : ℝ) (hc2_nn : 0 ≤ c2) (hc3_nn : 0 ≤ c3) : ‖c1 • b + √c2 • en - √c3 • ppg‖ ^ 2 = c1 ^ 2 * ‖b‖ ^ 2 + c2 * ‖en‖ ^ 2 + c3 * ‖ppg‖ ^ 2 + 2 * c1 * √c2 * inner ℝ b en - 2 * c1 * √c3 * inner ℝ b ppg - 2 * √c2 * √c3 * inner ℝ en ppg

Norm of un = b + √μ'•en

theorem PLAcceleratedNesterovLean.norm_two_term_sq {d : ℕ} (b en : E d) (c : ℝ) (hc : 0 ≤ c) : ‖b + √c • en‖ ^ 2 = ‖b‖ ^ 2 + c * ‖en‖ ^ 2 + 2 * √c * inner ℝ b en

Segment-based combined bound

theorem PLAcceleratedNesterovLean.combined_aim_segment (Fn ipGE sqη_ipGV μ'_half_Esq εη_half_Vsq : ℝ) (h_seg : Fn + sqη_ipGV ≥ ipGE - μ'_half_Esq - εη_half_Vsq) : Fn + sqη_ipGV - ipGE + μ'_half_Esq ≥ -εη_half_Vsq

From strong aiming and segment estimate: F(xn) + √η·⟨g,v⟩ - ⟨g,e⟩ + μ'/2·‖e‖² ≥ -εη/2·‖v‖²