From 7972dc147a181fede567fc3c577a4097495048d8 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Sun, 26 Jul 2026 22:46:31 -0400 Subject: [PATCH 1/4] feat: characterize least-squares residuals --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index d9ed9660d2ea58..20deb77cdbe141 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -202,6 +202,20 @@ theorem orthogonal_range (T : E →L[𝕜] F) : T.rangeᗮ = T†.ker := by rw [← T†.ker.orthogonal_orthogonal, T†.orthogonal_ker] simp +/-- The fitted value `A x` minimizes the distance to `y` among points in `A.range` +if and only if the adjoint of `A` sends the residual `y - A x` to zero. -/ +theorem norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero + (A : E →L[𝕜] F) (y : F) (x : E) : + (‖y - A x‖ = ⨅ z : A.range, ‖y - z‖) ↔ (A†) (y - A x) = 0 := by + -- The fitted value belongs to the range of `A`, with preimage `x`. + have hx : A x ∈ A.range := ⟨x, rfl⟩ + -- Rewrite minimization as orthogonality, then as membership in the kernel + -- of the adjoint, and finally as the adjoint sending the residual to zero. + rw [A.range.norm_eq_iInf_iff_inner_eq_zero hx, + ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker] + -- These expressions differ only by the coercion to an underlying linear map. + rfl + omit [CompleteSpace E] in theorem ker_le_ker_iff_range_le_range [FiniteDimensional 𝕜 E] {T U : E →L[𝕜] E} (hT : T.IsSymmetric) (hU : U.IsSymmetric) : From 03f6985e21ae738596c1a6a5776b0d82c126d72a Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Sun, 26 Jul 2026 23:24:28 -0400 Subject: [PATCH 2/4] feat: characterize least-squares minimizers --- .../Analysis/InnerProductSpace/Adjoint.lean | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 20deb77cdbe141..7f02f3c41e1528 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -216,6 +216,38 @@ theorem norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero -- These expressions differ only by the coercion to an underlying linear map. rfl +/-- The residual norm at `x` is minimal among all points of `E` if and only if +the adjoint of `A` sends the residual `y - A x` to zero. -/ +theorem forall_norm_sub_apply_le_iff_adjoint_apply_sub_eq_zero + (A : E →L[𝕜] F) (y : F) (x : E) : + (∀ z : E, ‖y - A x‖ ≤ ‖y - A z‖) ↔ (A†) (y - A x) = 0 := by + -- Residual norms are bounded below by zero. This fact lets us compare their + -- conditional infimum with any particular residual norm. + have residual_norms_bddBelow : + BddBelow (Set.range fun w : A.range => ‖y - w‖) := + ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ + -- Rewrite the adjoint equation as minimization over `A.range`. + rw [← A.norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero y x] + constructor + · intro h + apply le_antisymm + · -- The hypothesis makes the residual at `x` a lower bound for all + -- residuals coming from points in `A.range`. + apply le_ciInf + intro w + -- Since `w` belongs to `A.range`, it equals `A z` for some `z : E`. + obtain ⟨z, hz⟩ := w.property + rw [← hz] + exact h z + · -- The infimum is at most the residual at the particular range point + -- `A x`. + exact ciInf_le residual_norms_bddBelow ⟨A x, ⟨x, rfl⟩⟩ + · intro h z + -- The fitted value `A z` is an admissible point of `A.range`, so its + -- residual norm is at least the infimum. + rw [h] + exact ciInf_le residual_norms_bddBelow ⟨A z, ⟨z, rfl⟩⟩ + omit [CompleteSpace E] in theorem ker_le_ker_iff_range_le_range [FiniteDimensional 𝕜 E] {T U : E →L[𝕜] E} (hT : T.IsSymmetric) (hU : U.IsSymmetric) : From cd5ea7399be9d53d72e8e693c3e251abc15e7547 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Mon, 27 Jul 2026 01:47:45 -0400 Subject: [PATCH 3/4] refactor: simplify least-squares proofs --- .../Analysis/InnerProductSpace/Adjoint.lean | 32 ++++--------------- 1 file changed, 6 insertions(+), 26 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 7f02f3c41e1528..71aad92b4da4f4 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -207,44 +207,24 @@ if and only if the adjoint of `A` sends the residual `y - A x` to zero. -/ theorem norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero (A : E →L[𝕜] F) (y : F) (x : E) : (‖y - A x‖ = ⨅ z : A.range, ‖y - z‖) ↔ (A†) (y - A x) = 0 := by - -- The fitted value belongs to the range of `A`, with preimage `x`. - have hx : A x ∈ A.range := ⟨x, rfl⟩ - -- Rewrite minimization as orthogonality, then as membership in the kernel - -- of the adjoint, and finally as the adjoint sending the residual to zero. - rw [A.range.norm_eq_iInf_iff_inner_eq_zero hx, - ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker] - -- These expressions differ only by the coercion to an underlying linear map. - rfl + rw [A.range.norm_eq_iInf_iff_inner_eq_zero (by simp), + ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker, coe_coe, map_sub] /-- The residual norm at `x` is minimal among all points of `E` if and only if the adjoint of `A` sends the residual `y - A x` to zero. -/ theorem forall_norm_sub_apply_le_iff_adjoint_apply_sub_eq_zero (A : E →L[𝕜] F) (y : F) (x : E) : (∀ z : E, ‖y - A x‖ ≤ ‖y - A z‖) ↔ (A†) (y - A x) = 0 := by - -- Residual norms are bounded below by zero. This fact lets us compare their - -- conditional infimum with any particular residual norm. - have residual_norms_bddBelow : - BddBelow (Set.range fun w : A.range => ‖y - w‖) := + have residual_norms_bddBelow : BddBelow (Set.range fun w : A.range => ‖y - w‖) := ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ - -- Rewrite the adjoint equation as minimization over `A.range`. rw [← A.norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero y x] constructor · intro h apply le_antisymm - · -- The hypothesis makes the residual at `x` a lower bound for all - -- residuals coming from points in `A.range`. - apply le_ciInf - intro w - -- Since `w` belongs to `A.range`, it equals `A z` for some `z : E`. - obtain ⟨z, hz⟩ := w.property - rw [← hz] - exact h z - · -- The infimum is at most the residual at the particular range point - -- `A x`. - exact ciInf_le residual_norms_bddBelow ⟨A x, ⟨x, rfl⟩⟩ + · apply le_ciInf + simpa + · exact ciInf_le residual_norms_bddBelow ⟨A x, ⟨x, rfl⟩⟩ · intro h z - -- The fitted value `A z` is an admissible point of `A.range`, so its - -- residual norm is at least the infimum. rw [h] exact ciInf_le residual_norms_bddBelow ⟨A z, ⟨z, rfl⟩⟩ From 322cf58a29789aa2fc768adfd55317498517783f Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Mon, 27 Jul 2026 02:03:42 -0400 Subject: [PATCH 4/4] style: format least-squares theorem declaration --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 71aad92b4da4f4..c581d3440f858d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -204,8 +204,7 @@ theorem orthogonal_range (T : E →L[𝕜] F) : T.rangeᗮ = T†.ker := by /-- The fitted value `A x` minimizes the distance to `y` among points in `A.range` if and only if the adjoint of `A` sends the residual `y - A x` to zero. -/ -theorem norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero - (A : E →L[𝕜] F) (y : F) (x : E) : +theorem norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero (A : E →L[𝕜] F) (y : F) (x : E) : (‖y - A x‖ = ⨅ z : A.range, ‖y - z‖) ↔ (A†) (y - A x) = 0 := by rw [A.range.norm_eq_iInf_iff_inner_eq_zero (by simp), ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker, coe_coe, map_sub]