feat(Analysis/InnerProductSpace/Adjoint): characterize least-squares minimizers

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -202,6 +202,31 @@ 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
+  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
+  have residual_norms_bddBelow : BddBelow (Set.range fun w : A.range => ‖y - w‖) :=
+    ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩
+  rw [← A.norm_sub_apply_eq_iInf_iff_adjoint_apply_sub_eq_zero y x]
+  constructor
+  · intro h
+    apply le_antisymm
+    · apply le_ciInf
+      simpa
+    · exact ciInf_le residual_norms_bddBelow ⟨A x, ⟨x, rfl⟩⟩
+  · intro h z
+    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) :