Least-squares solutions

IsLeastSquares A b x says x minimises ‖A y − b‖ over the domain of a linear map A into a real inner product space. Mathlib provides the subspace side (Submodule.starProjection and its minimality); this file packages the pulled-back problem: the first-order characterisation, existence, uniqueness of fitted values, and the solution coset.

[UPSTREAM] candidate — mathlib has the ingredients but not the packaging; generalises from ℝ to RCLike 𝕜.

Main declarations

• IsLeastSquares A b x: x minimises ‖A y − b‖.
• isLeastSquares_iff_inner_eq_zero: the first-order characterisation — the residual is orthogonal to the range of A (the normal equations).
• exists_isLeastSquares: solutions exist whenever the range of A admits an orthogonal projection (in particular in finite dimension).
• IsLeastSquares.map_eq: fitted values are unique.
• IsLeastSquares.iff_map_eq: the solutions are exactly the preimages of the fitted value.

def Core.IsLeastSquares {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : E →ₗ[ℝ] F) (b : F) (x : E) : Prop

x is a least-squares solution of A y ≈ b if it minimises the residual norm ‖A y − b‖.

Equations

• Core.IsLeastSquares A b x = ∀ (y : E), ‖A x - b‖ ≤ ‖A y - b‖

theorem Core.isLeastSquares_iff_inner_eq_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x : E} : IsLeastSquares A b x ↔ ∀ (y : E), inner ℝ (b - A x) (A y) = 0

The first-order characterisation of least squares: x is a solution iff the residual b − A x is orthogonal to everything A can produce — the normal equations, with no rank hypothesis.

theorem Core.exists_isLeastSquares {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} [A.range.HasOrthogonalProjection] : ∃ (x : E), IsLeastSquares A b x

Least-squares solutions exist whenever the range of A admits an orthogonal projection — in particular whenever it is finite-dimensional.

theorem Core.IsLeastSquares.map_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x x' : E} (hx : IsLeastSquares A b x) (hx' : IsLeastSquares A b x') : A x = A x'

Fitted values are unique: any two least-squares solutions produce the same point of the range.

theorem Core.IsLeastSquares.iff_map_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x x' : E} (hx : IsLeastSquares A b x) : IsLeastSquares A b x' ↔ A x' = A x

The least-squares solutions are exactly the preimages of the fitted value: given one solution, another point solves iff it maps to the same place.

theorem Core.IsLeastSquares.eq_of_injective {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} (hA : Function.Injective ⇑A) {x x' : E} (hx : IsLeastSquares A b x) (hx' : IsLeastSquares A b x') : x = x'

Under an injective design map the least-squares solution is unique.