Curvature Absorption Assembly

Standalone proof that the curvature + projector-freezing perturbation is absorbable. Extracted from the main theorem to keep its proof term small (avoids kernel slowdown).

The key idea: Dπ is continuous at m⋆, so for small enough R, all perturbation terms are O(ε₁ · Ln) with ε₁ = sup ‖Dπ-P‖ → 0.

theorem PLAcceleratedNesterovLean.curv_absorb_assembly {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (L : NNReal) (hL : 0 < ↑L) (μ' : ℝ) (hμ' : 0 < μ') (θ : ℝ) (hθ_pos : 0 < θ) (η ρ : ℝ) (hη_pos : 0 < η) (hμη_lt1 : μ' * η < 1) (hρ_eq : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (S : Set (EuclideanSpace ℝ (Fin d))) (π : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (P : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (hP_ortho : ∀ (v : EuclideanSpace ℝ (Fin d)), ‖v‖ ^ 2 = ‖P v‖ ^ 2 + ‖v - P v‖ ^ 2) (mstar : EuclideanSpace ℝ (Fin d)) (hmstar : mstar ∈ S) (hP_eq : P = fderiv ℝ π mstar) (U_plus : Set (EuclideanSpace ℝ (Fin d))) (hU_open : IsOpen U_plus) (hm_in : mstar ∈ U_plus) (U : Set (EuclideanSpace ℝ (Fin d))) (hU_isopen : IsOpen U) (hU_sub : closure U_plus ⊆ U) (hf_lip : LipschitzOnWith L (gradient f) U) (hS_sub_U : S ⊆ U) (hmstar_U : mstar ∈ U) (hπ_on_U : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (hDπ_cont : ContinuousAt (fun (x : EuclideanSpace ℝ (Fin d)) => fderiv ℝ π x) mstar) (C_coer : ℝ) (hC_coer : 0 < C_coer) (hcoer_bound : ∀ (x₁ : EuclideanSpace ℝ (Fin d)) (n : ℕ), (nesterovSeq f η ρ x₁ n).x ∈ U_plus → (nesterovSeq f η ρ x₁ n).lookahead η ∈ U_plus → ‖(nesterovSeq f η ρ x₁ n).v‖ ^ 2 + μ' * ‖normalDisp π f η ρ x₁ n‖ ^ 2 ≤ C_coer * lyapunov P μ' π f η ρ x₁ n) (hπ_kills_normal : ∀ x ∈ U_plus, (fderiv ℝ π (π x)) (x - π x) = 0) (hgrad_zero : ∀ x ∈ S, gradient f x = 0) (hπ_diff_near : ∃ δ_diff > 0, ∀ z ∈ Metric.ball mstar δ_diff, DifferentiableAt ℝ π z) : ∃ (R_abs : ℝ), 0 < R_abs ∧ ∀ (x₁ : EuclideanSpace ℝ (Fin d)) (n : ℕ), (nesterovSeq f η ρ x₁ n).x ∈ Metric.ball mstar R_abs → (nesterovSeq f η ρ x₁ n).lookahead η ∈ Metric.ball mstar R_abs → lyapunov P μ' π f η ρ x₁ n ≤ R_abs ^ 2 → have sn := nesterovSeq f η ρ x₁ n; have gn := gradient f (sn.lookahead η); have en := sn.lookahead η - π (sn.lookahead η); have ξn := curvatureError (⇑P) π f η ρ x₁ n; have un1 := auxVar P μ' π f η ρ x₁ (n + 1); have wn := un1 - √μ' • ξn; have δ_curv := √μ' * inner ℝ wn ξn + √μ' ^ 2 / 2 * ‖ξn‖ ^ 2; have a := √(μ' * η); have Ln := lyapunov P μ' π f η ρ x₁ n; have proj_err := a * |inner ℝ gn (P en)|; δ_curv + proj_err ≤ θ * a * Ln

Public theorem wrapper for curvAbsorbAssemblyProof.

theorem PLAcceleratedNesterovLean.curv_absorb_assembly_gen {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (L : NNReal) (hL : 0 < ↑L) (μ' : ℝ) (hμ' : 0 < μ') (θ : ℝ) (hθ_pos : 0 < θ) (η ρ : ℝ) (hη_pos : 0 < η) (hμη_lt1 : μ' * η < 1) (hρ_eq : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (S : Set (EuclideanSpace ℝ (Fin d))) (π : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (P : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (hP_ortho : ∀ (v : EuclideanSpace ℝ (Fin d)), ‖v‖ ^ 2 = ‖P v‖ ^ 2 + ‖v - P v‖ ^ 2) (mstar : EuclideanSpace ℝ (Fin d)) (hmstar : mstar ∈ S) (hP_eq : P = fderiv ℝ π mstar) (U_plus : Set (EuclideanSpace ℝ (Fin d))) (hU_open : IsOpen U_plus) (hm_in : mstar ∈ U_plus) (U : Set (EuclideanSpace ℝ (Fin d))) (hU_isopen : IsOpen U) (hU_sub : closure U_plus ⊆ U) (hf_lip : LipschitzOnWith L (gradient f) U) (hS_sub_U : S ⊆ U) (hmstar_U : mstar ∈ U) (hπ_on_U : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (hDπ_cont : ContinuousAt (fun (x : EuclideanSpace ℝ (Fin d)) => fderiv ℝ π x) mstar) (C_coer : ℝ) (hC_coer : 0 < C_coer) (hcoer_bound : ∀ (s : NesterovState d), s.x ∈ U_plus → s.lookahead η ∈ U_plus → ‖s.v‖ ^ 2 + μ' * ‖normalDispOfState π η s‖ ^ 2 ≤ C_coer * lyapunovOfState P μ' π f η s) (hπ_kills_normal : ∀ x ∈ U_plus, (fderiv ℝ π (π x)) (x - π x) = 0) (hgrad_zero : ∀ x ∈ S, gradient f x = 0) (hπ_diff_near : ∃ δ_diff > 0, ∀ z ∈ Metric.ball mstar δ_diff, DifferentiableAt ℝ π z) : ∃ (R_abs : ℝ), 0 < R_abs ∧ ∀ (s₀ : NesterovState d) (n : ℕ), (nesterovSeqGen f η ρ s₀ n).x ∈ Metric.ball mstar R_abs → (nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Metric.ball mstar R_abs → lyapunovOfState P μ' π f η (nesterovSeqGen f η ρ s₀ n) ≤ R_abs ^ 2 → have sn := nesterovSeqGen f η ρ s₀ n; have gn := gradient f (sn.lookahead η); have en := sn.lookahead η - π (sn.lookahead η); have ξn := curvatureErrorOfState (⇑P) π f η ρ sn; have un1 := auxVarOfState P μ' π η (nesterovStep f η ρ sn); have wn := un1 - √μ' • ξn; have δ_curv := √μ' * inner ℝ wn ξn + √μ' ^ 2 / 2 * ‖ξn‖ ^ 2; have a := √(μ' * η); have Ln := lyapunovOfState P μ' π f η sn; have proj_err := a * |inner ℝ gn (P en)|; δ_curv + proj_err ≤ θ * a * Ln

Public theorem wrapper for curvAbsorbAssemblyGenProof.