noncomputable def reducedProjection {n k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) : Matrix (Fin n) (Fin n) ℝ

The affine map P = I - G Z (Zᵀ G Z)⁻¹ Zᵀ from (9.3.31).

theorem reducedProjection_eq {n k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) : reducedProjection G Z = 1 - G * Z * (Z.transpose * G * Z)⁻¹ * Z.transpose

Unfolding reducedProjection G Z gives the source formula (9.3.31).

theorem inverse_kkt_pair_satisfies_rhs {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (rhs₁ : Fin n → ℝ) (rhs₂ : Fin m → ℝ) (hA : Function.Injective A.mulVec) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : have y := (kktMatrix G A)⁻¹.mulVec (Sum.elim rhs₁ rhs₂); SatisfiesEqualityConstrainedQpKKTSystem G A rhs₁ rhs₂ (y ∘ Sum.inl) (y ∘ Sum.inr)

Helper for Chapter09 Exercise 9.12: applying the inverse KKT matrix to a block right-hand side produces a primal-dual pair satisfying the corresponding KKT system.

theorem primal_solution_of_zero_dual_rhs_eq_nullspace_formula {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) {p x : Fin n → ℝ} {lam : Fin m → ℝ} (hSystem : SatisfiesEqualityConstrainedQpKKTSystem G A p 0 x lam) : x = (Z * (Z.transpose * G * Z)⁻¹ * Z.transpose).mulVec p

Helper for Chapter09 Exercise 9.12: every KKT solution with zero dual right-hand side has its primal component given by the reduced-space null-space formula.

theorem inverse_pure_primal_primal_component_eq_u_block {n m : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (p : Fin n → ℝ) : (kktMatrix G A)⁻¹.mulVec (Sum.elim p 0) ∘ Sum.inl = (kktInverseU G A).mulVec p

Helper for Chapter09 Exercise 9.12: the primal component of the inverse-KKT action on a pure primal right-hand side is exactly the U block action.

theorem kkt_inverse_u_mulVec_eq_nullspace_formula {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hA : Function.Injective A.mulVec) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) (p : Fin n → ℝ) : (kktInverseU G A).mulVec p = (Z * (Z.transpose * G * Z)⁻¹ * Z.transpose).mulVec p

Helper for Chapter09 Exercise 9.12: the U block acts on every primal right-hand side by the reduced-space null-space formula.

theorem kktInverseU_eq_nullSpaceFormula {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hA : Function.Injective A.mulVec) (hGsym : G.IsSymm) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : kktInverseU G A = Z * (Z.transpose * G * Z)⁻¹ * Z.transpose

Chapter09 Exercise 9.12 (1): if A has full column rank, G is symmetric, Z spans ker Aᵀ, and the reduced Hessian Zᵀ G Z is positive definite, then the U block of (kktMatrix G A)⁻¹ is Z (Zᵀ G Z)⁻¹ Zᵀ, i.e. formula (9.3.58).

theorem reducedProjection_transpose_eq {n k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hGsym : G.IsSymm) (hReduced : (Z.transpose * G * Z).PosDef) : (reducedProjection G Z).transpose = 1 - Z * (Z.transpose * G * Z)⁻¹ * Z.transpose * G

Helper for Chapter09 Exercise 9.12: transposing the generalized projector rewrites it into the source formula I - Z (Zᵀ G Z)⁻¹ Zᵀ G.

theorem reducedProjection_transpose_mul_reducedBasis_eq_zero {n k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hGsym : G.IsSymm) (hReduced : (Z.transpose * G * Z).PosDef) : (reducedProjection G Z).transpose * Z = 0

Helper for Chapter09 Exercise 9.12: the transpose of the generalized projector annihilates the reduced null-space basis Z.

theorem reducedProjection_transpose_mul_leftInverse_mul_constraintTranspose_eq {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A Y : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hGsym : G.IsSymm) (hY : A.transpose * Y = 1) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : (reducedProjection G Z).transpose * Y * A.transpose = (reducedProjection G Z).transpose

Helper for Chapter09 Exercise 9.12: after applying the transpose projector, the left inverse Y reconstructs the same projected vector from its constraint image.

theorem dual_rhs_solution_has_generalized_elimination_form {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A Y : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (q : Fin m → ℝ) (hA : Function.Injective A.mulVec) (hGsym : G.IsSymm) (hY : A.transpose * Y = 1) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : SatisfiesEqualityConstrainedQpKKTSystem G A 0 q ((-(reducedProjection G Z).transpose * Y).mulVec q) ((-Y.transpose * G * (reducedProjection G Z).transpose * Y).mulVec q)

Helper for Chapter09 Exercise 9.12: the generalized-elimination formulas produce a KKT solution for every pure dual right-hand side (0, q).

theorem inverse_pure_dual_components_eq_w_t_blocks {n m : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin m) ℝ) (q : Fin m → ℝ) : (kktMatrix G A)⁻¹.mulVec (Sum.elim 0 q) ∘ Sum.inl = (kktInverseW G A).mulVec q ∧ (kktMatrix G A)⁻¹.mulVec (Sum.elim 0 q) ∘ Sum.inr = (kktInverseT G A).mulVec q

Helper for Chapter09 Exercise 9.12: the pure-dual inverse-KKT action splits into the W and T block actions on the primal and multiplier components.

theorem dual_rhs_inverse_blocks_mulVec_eq_generalized_elimination {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A Y : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (q : Fin m → ℝ) (hA : Function.Injective A.mulVec) (hGsym : G.IsSymm) (hY : A.transpose * Y = 1) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : (kktInverseW G A).mulVec q = (-(reducedProjection G Z).transpose * Y).mulVec q ∧ (kktInverseT G A).mulVec q = (-Y.transpose * G * (reducedProjection G Z).transpose * Y).mulVec q

Helper for Chapter09 Exercise 9.12: the inverse KKT blocks acting on a pure dual right-hand side agree with the generalized-elimination formulas for both the primal and multiplier components.

theorem kktInverseW_eq_neg_projectionTranspose_mul_leftInverse {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A Y : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hA : Function.Injective A.mulVec) (hGsym : G.IsSymm) (hY : A.transpose * Y = 1) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : kktInverseW G A = -(reducedProjection G Z).transpose * Y

Chapter09 Exercise 9.12 (2): under the same generalized-elimination hypotheses, the W block of (kktMatrix G A)⁻¹ is -Pᵀ Y, where P = reducedProjection G Z, G is symmetric, and Y satisfies Aᵀ Y = I, i.e. formula (9.3.59).

theorem kktInverseT_eq_neg_leftInverseTranspose_mul_hessian_mul_projectionTranspose_mul_leftInverse {n m k : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (A Y : Matrix (Fin n) (Fin m) ℝ) (Z : Matrix (Fin n) (Fin k) ℝ) (hA : Function.Injective A.mulVec) (hGsym : G.IsSymm) (hY : A.transpose * Y = 1) (hZ : IsReducedNullMatrix A Z) (hReduced : (Z.transpose * G * Z).PosDef) : kktInverseT G A = -Y.transpose * G * (reducedProjection G Z).transpose * Y

Chapter09 Exercise 9.12 (3): under the same generalized-elimination hypotheses, the T block of (kktMatrix G A)⁻¹ is -Yᵀ G Pᵀ Y, where P = reducedProjection G Z, G is symmetric, and Y satisfies Aᵀ Y = I, i.e. formula (9.3.60).