Least-squares solutions

IsLeastSquares A b x says x minimises the residual norm ‖b − A y‖ over the domain of a linear map A between real inner product spaces. Mathlib characterises the minimisers of a continuous linear map by its adjoint (ContinuousLinearMap.forall_norm_sub_apply_le_iff_adjoint_apply_sub_eq_zero); in finite dimension every linear map is continuous, and this file packages the resulting API: the normal equations in adjoint and inner-product form, existence by orthogonal projection, uniqueness of fitted values, and the solution coset.

[UPSTREAM] candidate; generalises from ℝ to RCLike 𝕜.

Main declarations

• IsLeastSquares A b x: x minimises ‖b − A y‖.
• isLeastSquares_iff_adjoint_eq_zero, isLeastSquares_iff_inner_eq_zero: the normal equations — the adjoint kills the residual, equivalently the residual is orthogonal to the range of A.
• exists_isLeastSquares, isLeastSquares_of_map_eq: solutions exist, and an interpolating point is one.
• IsLeastSquares.map_eq, IsLeastSquares.iff_map_eq: fitted values are unique, and the solutions are exactly the preimages of the fitted value.

def Core.IsLeastSquares {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ 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 ‖b − A y‖.

Equations

• Core.IsLeastSquares A b x = IsMinOn (fun (y : E) => ‖b - A y‖) Set.univ x

theorem Core.isLeastSquares_of_map_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x : E} (h : A x = b) : IsLeastSquares A b x

An interpolating point is a least-squares solution.

theorem Core.isLeastSquares_iff_adjoint_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x : E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] : IsLeastSquares A b x ↔ (LinearMap.adjoint A) (b - A x) = 0

The normal equations in adjoint form: x solves iff the adjoint kills the residual.

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

The normal equations in inner-product form: the residual is orthogonal to the range.

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

Least-squares solutions exist.

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

Fitted values are unique: any two least-squares solutions map to the same point.

theorem Core.IsLeastSquares.iff_map_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : E →ₗ[ℝ] F} {b : F} {x x' : E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (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.

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

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