noncomputable def bfgsMatrixDifference {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) : Matrix (Fin n) (Fin n) ℝ

Definition 1.8.14: ΔHₖ is the Broyden--Fletcher--Goldfarb--Shanno (BFGS) correction (βₖ / ⟪γₖ, δₖ⟫) δₖ δₖᵀ - (Hₖ γₖ δₖᵀ + δₖ γₖᵀ Hₖ) / ⟪γₖ, δₖ⟫, where βₖ = 1 + ⟪Hₖ γₖ, γₖ⟫ / ⟪γₖ, δₖ⟫. The curvature hypotheses belong on the secant and positivity theorems rather than on this source-facing matrix formula.

theorem bfgsMatrixDifference_toEuclideanLin {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) : Matrix.toEuclideanLin (bfgsMatrixDifference Hk γk δk) = ↑(have H := Matrix.toEuclideanLin Hk; have rho := (inner ℝ γk δk)⁻¹; have hγ := H γk; have beta := 1 + inner ℝ hγ γk * rho; (beta * rho) • ((InnerProductSpace.rankOne ℝ) δk) δk - rho • (((InnerProductSpace.rankOne ℝ) hγ) δk + ((InnerProductSpace.rankOne ℝ) δk) ((LinearMap.adjoint H) γk)))

The BFGS correction matrix realizes the canonical operator-level BFGS formula on Euclidean space.

noncomputable def bfgsUpdatedMatrix {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) : Matrix (Fin n) (Fin n) ℝ

The BFGS update defines the next inverse-Hessian approximation by Hₖ₊₁ = Hₖ + ΔHₖ.

theorem inner_adjoint_apply_self_eq_inner_apply_self {n : ℕ} (H : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (γ : EuclideanSpace ℝ (Fin n)) : inner ℝ ((LinearMap.adjoint H) γ) γ = inner ℝ γ (H γ)

Helper for Definition 1.8.14: evaluating the adjoint on the same vector recovers the same quadratic scalar as evaluating the original map.

theorem bfgsUpdatedMatrix_toEuclideanLin {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) : Matrix.toEuclideanLin (bfgsUpdatedMatrix Hk γk δk) = have H := Matrix.toEuclideanLin Hk; have rho := (inner ℝ γk δk)⁻¹; have hγ := H γk; have beta := 1 + inner ℝ hγ γk * rho; H + (beta * rho) • ↑(((InnerProductSpace.rankOne ℝ) δk) δk) - rho • (↑(((InnerProductSpace.rankOne ℝ) hγ) δk) + ↑(((InnerProductSpace.rankOne ℝ) δk) ((LinearMap.adjoint H) γk)))

Helper for Definition 1.8.14: the BFGS-updated matrix realizes the canonical operator-level BFGS formula on Euclidean space.

theorem isSymm_inner_toEuclideanLin_swap {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (hHk : Hk.IsSymm) (x y : EuclideanSpace ℝ (Fin n)) : inner ℝ x ((Matrix.toEuclideanLin Hk) y) = inner ℝ ((Matrix.toEuclideanLin Hk) x) y

Helper for Definition 1.8.14: symmetry of Hₖ lets us swap Hₖ across the Euclidean inner product.

theorem bfgsUpdatedMatrix_toEuclideanLin_factorized {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) (hHk : Hk.IsSymm) : Matrix.toEuclideanLin (bfgsUpdatedMatrix Hk γk δk) = have H := Matrix.toEuclideanLin Hk; have rho := (inner ℝ γk δk)⁻¹; (1 - rho • ↑(((InnerProductSpace.rankOne ℝ) δk) γk)) * H * (1 - rho • ↑(((InnerProductSpace.rankOne ℝ) γk) δk)) + rho • ↑(((InnerProductSpace.rankOne ℝ) δk) δk)

Helper for Definition 1.8.14: when Hₖ is symmetric, the BFGS operator has the standard factorized form (I - ρ δ γᵀ) Hₖ (I - ρ γ δᵀ) + ρ δ δᵀ.

theorem bfgs_rankOne_perturbation_adjoint {n : ℕ} (γk δk : EuclideanSpace ℝ (Fin n)) (rho : ℝ) : 1 - rho • ↑(((InnerProductSpace.rankOne ℝ) δk) γk) = LinearMap.adjoint (1 - rho • ↑(((InnerProductSpace.rankOne ℝ) γk) δk))

Helper for Definition 1.8.14: the left BFGS rank-one perturbation is the adjoint of the corresponding right perturbation.

theorem posDef_inner_toEuclideanLin_pos {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (hHkPosDef : Hk.PosDef) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : 0 < inner ℝ x ((Matrix.toEuclideanLin Hk) x)

Helper for Definition 1.8.14: a positive-definite matrix yields a strictly positive Euclidean quadratic form on every nonzero vector.

theorem bfgsUpdatedMatrix_inner_pos {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) (hHkPosDef : Hk.PosDef) (hγδ : 0 < inner ℝ γk δk) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : 0 < inner ℝ x ((Matrix.toEuclideanLin (bfgsUpdatedMatrix Hk γk δk)) x)

Helper for Definition 1.8.14: a positive-definite Hₖ gives a strictly positive quadratic form for the updated BFGS operator under the curvature condition.

theorem bfgsUpdatedMatrix_isSymm {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) (hHk : Hk.IsSymm) : (bfgsUpdatedMatrix Hk γk δk).IsSymm

The BFGS updated matrix remains symmetric when the current quasi-Newton matrix is symmetric.

theorem inner_toEuclideanLin_eq_dotProduct_mulVec {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) : inner ℝ x ((Matrix.toEuclideanLin A) x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp

Helper for Definition 1.8.14: the Euclidean quadratic form of A.toEuclideanLin matches the matrix quadratic form xᵀ A x.

theorem bfgsUpdatedMatrix_posDef {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) (hHkPosDef : Hk.PosDef) (hγδ : 0 < inner ℝ γk δk) : (bfgsUpdatedMatrix Hk γk δk).PosDef

The BFGS updated matrix remains positive definite under the usual curvature condition.

theorem bfgs_secant_scalar_cleanup {a c : ℝ} (hc : c ≠ 0) : c * (c⁻¹ * (1 + c⁻¹ * a)) - c⁻¹ * a = 1

Helper for Definition 1.8.14: the scalar BFGS secant coefficient simplifies to 1 once the curvature denominator is nonzero.

theorem bfgsUpdatedMatrix_secantEquation {n : ℕ} (Hk : Matrix (Fin n) (Fin n) ℝ) (γk δk : EuclideanSpace ℝ (Fin n)) (hγδ : inner ℝ γk δk ≠ 0) : (Matrix.toEuclideanLin (bfgsUpdatedMatrix Hk γk δk)) γk = δk

The BFGS updated matrix satisfies the quasi-Newton secant equation whenever the curvature denominator is nonzero.

theorem bfgsUpdatedMatrix_step_secantEquation {n : ℕ} (xk xNext gk gNext : EuclideanSpace ℝ (Fin n)) (Hk : Matrix (Fin n) (Fin n) ℝ) (hcurvature : inner ℝ (gNext - gk) (xNext - xk) ≠ 0) : (Matrix.toEuclideanLin (bfgsUpdatedMatrix Hk (gNext - gk) (xNext - xk))) (gNext - gk) = xNext - xk

Specializing the BFGS secant equation to consecutive iterates and gradients uses only the curvature witness for that actual step data.