DataSpan.lean

1 import Mathlib.LinearAlgebra.Isomorphisms
2 import Mathlib.LinearAlgebra.Basis.VectorSpace
3 import Mathlib.Tactic
4 
5 /-! Algebraic data-span identification. The analytic Moore-Penrose adapter is separate. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Identification
8 variable {K X Y Z : Type*} [Field K]
9 variable [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y]
10 variable [AddCommGroup Z] [Module K Z]
11 
12 noncomputable def onRange (A : X →ₗ[K] Y) (B : X →ₗ[K] Z)
13     (h : LinearMap.ker A ≤ LinearMap.ker B) : LinearMap.range A →ₗ[K] Z :=
14   ((LinearMap.ker A).liftQ B h).comp A.quotKerEquivRange.symm.toLinearMap
15 
16 @[simp] theorem onRange_apply (A : X →ₗ[K] Y) (B : X →ₗ[K] Z)
17     (h : LinearMap.ker A ≤ LinearMap.ker B) (x : X) :
18     onRange A B h (A.rangeRestrict x) = B x := by
19   change (LinearMap.ker A).liftQ B h (A.quotKerEquivRange.symm ⟨A x, _⟩) = B x
20   rw [LinearMap.quotKerEquivRange_symm_apply_image]
21   rfl
22 
23 theorem fit_iff_kernel (A : X →ₗ[K] Y) (B : X →ₗ[K] Z) :
24     (∃ F : Y →ₗ[K] Z, F.comp A = B) ↔ LinearMap.ker A ≤ LinearMap.ker B := by
25   constructor
26   · rintro ⟨F, rfl⟩ x hx
27     change F (A x) = 0
28     rw [LinearMap.mem_ker.mp hx, map_zero]
29   · intro h
30     obtain ⟨F,hF⟩ := (onRange A B h).exists_extend
31     refine ⟨F, ?_⟩
32     apply LinearMap.ext
33     intro x
34     have hx := congrArg (fun G : LinearMap.range A →ₗ[K] Z => G (A.rangeRestrict x)) hF
35     simpa using hx
36 
37 theorem fits_agree_on_range (A : X →ₗ[K] Y) (B : X →ₗ[K] Z)
38     (F G : Y →ₗ[K] Z) (hF : F.comp A = B) (hG : G.comp A = B)
39     (y : Y) (hy : y ∈ LinearMap.range A) : F y = G y := by
40   obtain ⟨x,rfl⟩ := hy
41   exact (congrArg (fun H : X →ₗ[K] Z => H x) hF).trans
42     (congrArg (fun H : X →ₗ[K] Z => H x) hG).symm
43 
44 theorem fitted_range (A : X →ₗ[K] Y) (B : X →ₗ[K] Y)
45     (F : Y →ₗ[K] Y) (hF : F.comp A = B) :
46     (∀ y ∈ LinearMap.range A, F y ∈ LinearMap.range A) ↔
47       LinearMap.range B ≤ LinearMap.range A := by
48   constructor
49   · intro h y hy
50     obtain ⟨x,rfl⟩ := hy
51     rw [← hF]
52     exact h (A x) ⟨x,rfl⟩
53   · intro h y hy
54     obtain ⟨x,rfl⟩ := hy
55     apply h
56     exact ⟨x, congrArg (fun H : X →ₗ[K] Y => H x) hF |>.symm⟩
57 
58 theorem generalized_inverse_fit (A : X →ₗ[K] Y) (B : X →ₗ[K] Z)
59     (J : Y →ₗ[K] X) (h : LinearMap.ker A ≤ LinearMap.ker B)
60     (hJ : A.comp (J.comp A) = A) : (B.comp J).comp A = B := by
61   apply LinearMap.ext
62   intro x
63   have hx : x - J (A x) ∈ LinearMap.ker A := by
64     change A (x - J (A x)) = 0
65     rw [map_sub]
66     exact sub_eq_zero.mpr (congrArg (fun F : X →ₗ[K] Y => F x) hJ).symm
67   have hb := LinearMap.mem_ker.mp (h hx)
68   rw [map_sub] at hb
69   exact (sub_eq_zero.mp hb).symm
70 
71 theorem unseen_direction_not_identified (W : Submodule K Y) (y : Y) (hy : y ∉ W)
72     (F : Y →ₗ[K] Y) : ∃ G : Y →ₗ[K] Y,
73       (∀ w ∈ W, F w = G w) ∧ F y ≠ G y := by
74   have yn : y ≠ 0 := fun hz => hy (hz ▸ W.zero_mem)
75   obtain ⟨G,hG,hGy⟩ := (F.comp W.subtype).exists_extend_of_notMem hy (F y + y)
76   refine ⟨G, ?_, ?_⟩
77   · intro w hw
78     exact (congrArg (fun H : W →ₗ[K] Y => H ⟨w,hw⟩) hG).symm
79   · rw [hGy]
80     exact fun he => yn (add_left_cancel (show F y + y = F y + 0 by simpa using he.symm))
81 
82 end Komorebi.LSM.Identification

Back to source controls