Pseudoinverse.lean

1 import KomorebiLSM.DataSpan
2 import Mathlib.Analysis.InnerProductSpace.Adjoint
3 import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
4 
5 /-! Canonical finite-dimensional orthogonal generalized inverse. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Identification
8 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
9 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
10 variable [FiniteDimensional ℝ E]
11 
12 noncomputable def retained (A : E →ₗ[ℝ] F) : E →ₗ[ℝ] E :=
13   A.kerᗮ.starProjection.toLinearMap
14 
15 theorem retained_apply (A : E →ₗ[ℝ] F) (x : E) :
16     retained A x = x - A.ker.starProjection x := by
17   exact Submodule.starProjection_orthogonal_val _
18 
19 theorem retained_kernel (A : E →ₗ[ℝ] F) : A.ker ≤ (retained A).ker := by
20   intro x hx
21   change retained A x = 0
22   rw [retained_apply, A.ker.starProjection_eq_self_iff.mpr hx, sub_self]
23 
24 noncomputable def pinv (A : E →ₗ[ℝ] F) : F →ₗ[ℝ] E :=
25   (onRange A (retained A) (retained_kernel A)).comp A.range.orthogonalProjectionOnto.toLinearMap
26 
27 @[simp] theorem pinv_apply_image (A : E →ₗ[ℝ] F) (x : E) :
28     pinv A (A x) = retained A x := by
29   change onRange A (retained A) (retained_kernel A) (A.range.orthogonalProjectionOnto (A x)) = _
30   have he : A.range.orthogonalProjectionOnto (A x) = A.rangeRestrict x :=
31     A.range.orthogonalProjectionOnto_mem_subspace_eq_self (A.rangeRestrict x)
32   rw [he, onRange_apply]
33 
34 theorem apply_retained (A : E →ₗ[ℝ] F) (x : E) : A (retained A x) = A x := by
35   rw [retained_apply, map_sub]
36   have hz : A (A.ker.starProjection x) = 0 := A.ker.starProjection_apply_mem x
37   rw [hz, sub_zero]
38 
39 theorem pinv_apply_mem (A : E →ₗ[ℝ] F) (y : F) : pinv A y ∈ A.kerᗮ := by
40   obtain ⟨x,hx⟩ := (A.range.orthogonalProjectionOnto y).property
41   have he : A.range.orthogonalProjectionOnto y = A.rangeRestrict x := Subtype.ext hx.symm
42   change onRange A (retained A) (retained_kernel A) (A.range.orthogonalProjectionOnto y) ∈ _
43   rw [he, onRange_apply]
44   exact A.kerᗮ.starProjection_apply_mem x
45 
46 theorem apply_pinv (A : E →ₗ[ℝ] F) (y : F) : A (pinv A y) = A.range.starProjection y := by
47   obtain ⟨x,hx⟩ := (A.range.orthogonalProjectionOnto y).property
48   have he : A.range.orthogonalProjectionOnto y = A.rangeRestrict x := Subtype.ext hx.symm
49   change A (onRange A (retained A) (retained_kernel A) (A.range.orthogonalProjectionOnto y)) = _
50   rw [he, onRange_apply, apply_retained]
51   exact hx
52 
53 theorem penrose_one (A : E →ₗ[ℝ] F) : A.comp ((pinv A).comp A) = A := by
54   apply LinearMap.ext
55   intro x
56   exact (congrArg A (pinv_apply_image A x)).trans (apply_retained A x)
57 
58 theorem penrose_two (A : E →ₗ[ℝ] F) : (pinv A).comp (A.comp (pinv A)) = pinv A := by
59   apply LinearMap.ext
60   intro y
61   change pinv A (A (pinv A y)) = _
62   rw [pinv_apply_image]
63   exact A.kerᗮ.starProjection_eq_self_iff.mpr (pinv_apply_mem A y)
64 
65 theorem penrose_range_projection (A : E →ₗ[ℝ] F) :
66     A.comp (pinv A) = A.range.starProjection.toLinearMap := by
67   apply LinearMap.ext
68   exact apply_pinv A
69 
70 theorem penrose_source_projection (A : E →ₗ[ℝ] F) :
71     (pinv A).comp A = A.kerᗮ.starProjection.toLinearMap := by
72   apply LinearMap.ext
73   exact pinv_apply_image A
74 
75 theorem moore_penrose_fit (A : E →ₗ[ℝ] F) (B : E →ₗ[ℝ] F)
76     (h : A.ker ≤ B.ker) : (B.comp (pinv A)).comp A = B :=
77   generalized_inverse_fit A B (pinv A) h (penrose_one A)
78 theorem penrose_three (A : E →ₗ[ℝ] F) : (A.comp (pinv A)).IsSymmetric := by
79   rw [penrose_range_projection]
80   exact A.range.starProjection_isSymmetric
81 
82 theorem penrose_four (A : E →ₗ[ℝ] F) : ((pinv A).comp A).IsSymmetric := by
83   rw [penrose_source_projection]
84   exact A.kerᗮ.starProjection_isSymmetric
85 end Komorebi.LSM.Identification

Back to source controls