InstrumentCoordinates.lean

1 import KomorebiLSM.InstrumentCompletion
2 import KomorebiLSM.NormalizedDefect
3 import Mathlib.LinearAlgebra.Basis.VectorSpace
4 
5 /-! Finite coordinates with the mass functional literally in coordinate zero.
6 The coordinate map is onto, its row space is exact, and branch maps are unique. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.FiniteInstruments
9 open scoped BigOperators
10 open Module FiniteBayes
11 
12 section AnchoredBasis
13 variable {E : Type*} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E]
14 
15 /-- Extend one specified nonzero vector and place it at the first finite index. -/
16 theorem exists_basis_first (w : E) (hw : w ≠ 0) :
17     ∃ (n : ℕ) (hn : 0 < n) (b : Basis (Fin n) ℝ E), b ⟨0,hn⟩ = w := by
18   classical
19   have hs : LinearIndepOn ℝ id ({w} : Set E) := (linearIndepOn_singleton_iff ℝ).mpr hw
20   let J := hs.extend (Set.subset_univ {w})
21   let b : Basis J ℝ E := Basis.extend hs
22   let : Fintype J := FiniteDimensional.fintypeBasisIndex b
23   let j0 : J := ⟨w, Basis.subset_extend hs (Set.mem_singleton w)⟩
24   have hn : 0 < Fintype.card J := Fintype.card_pos_iff.mpr ⟨j0⟩
25   let k0 : Fin (Fintype.card J) := ⟨0,hn⟩
26   let e0 := Fintype.equivFin J
27   let e := e0.trans (Equiv.swap (e0 j0) k0)
28   have he : e j0 = k0 := by simp [e]
29   refine ⟨Fintype.card J,hn,b.reindex e, ?_⟩
30   change (b.reindex e) k0 = w
31   rw [← he, Basis.reindex_apply, Equiv.symm_apply_apply]
32   exact Basis.extend_apply_self hs j0
33 
34 end AnchoredBasis
35 
36 section RowCoordinates
37 variable {X : Type*} [AddCommGroup X] [Module ℝ X]
38 variable {J : Type*} [Fintype J] {W : Submodule ℝ (Dual ℝ X)}
39 
40 omit [Fintype J] in
41 /-- Basis evaluation is surjective onto the finite coordinate space. -/
42 theorem basis_observation_surjective [FiniteDimensional ℝ X] (b : Basis J ℝ W) :
43     Function.Surjective (basisObservation b) := by
44   intro z
45   obtain ⟨x,hx⟩ := observableState_surjective W (b.constr ℝ z)
46   refine ⟨x, ?_⟩
47   funext j
48   have hj := congrArg (fun f : Dual ℝ W => f (b j)) hx
49   change (b j : Dual ℝ X) x = z j
50   simpa only [observableState_apply, Basis.constr_basis] using hj
51 
52 /-- The coordinate matrix has exactly the chosen observable row space. -/
53 theorem basis_observation_rowspace (b : Basis J ℝ W) :
54     LinearMap.range (basisObservation b).dualMap = W := by
55   classical
56   apply le_antisymm
57   · rintro r ⟨f,rfl⟩
58     have he : (basisObservation b).dualMap f =
59         ∑ j, f (pointMass j) • (b j : Dual ℝ X) := by
60       ext x
61       change f (basisObservation b x) = _
62       rw [vector_eq_sum_pointMass (basisObservation b x), map_sum]
63       simp only [map_smul, LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul]
64       apply Finset.sum_congr rfl
65       intro j _
66       exact mul_comm _ _
67     rw [he]
68     exact Submodule.sum_mem W (fun j _ => W.smul_mem _ (b j).property)
69   · intro r hr
70     refine ⟨basisRowReadout b ⟨r,hr⟩, ?_⟩
71     ext x
72     exact basisRowReadout_correct b ⟨r,hr⟩ x
73 
74 /-- A full-row-rank observation map makes its reduced operator unique. -/
75 theorem closed_operator_unique {E : Type*} [AddCommGroup E] [Module ℝ E]
76     (R : X →ₗ[ℝ] E) (hR : Function.Surjective R) (M : X →ₗ[ℝ] X)
77     (B D : E →ₗ[ℝ] E) (hB : B.comp R = R.comp M) (hD : D.comp R = R.comp M) :
78     D = B := by
79   ext z
80   obtain ⟨x,rfl⟩ := hR z
81   exact congrArg (fun f : X →ₗ[ℝ] E => f x) (hD.trans hB.symm)
82 
83 /-- Membership of each actual coordinate row contains the full row space. -/
84 theorem summary_rowspace_le (R : X →ₗ[ℝ] (J → ℝ))
85     (W : Submodule ℝ (Dual ℝ X))
86     (h : ∀ j, (LinearMap.proj j).comp R ∈ W) : LinearMap.range R.dualMap ≤ W := by
87   classical
88   rintro r ⟨f,rfl⟩
89   have he : R.dualMap f = ∑ j, f (pointMass j) • (LinearMap.proj j).comp R := by
90     apply LinearMap.ext
91     intro x
92     change f (R x) = _
93     rw [vector_eq_sum_pointMass (R x), map_sum]
94     simp only [map_smul, LinearMap.sum_apply, LinearMap.smul_apply,
95       LinearMap.comp_apply, LinearMap.proj_apply, smul_eq_mul]
96     apply Finset.sum_congr rfl
97     intro j _
98     exact mul_comm _ _
99   rw [he]
100   exact W.sum_mem (fun j _ => W.smul_mem _ (h j))
101 
102 end RowCoordinates
103 
104 section CompletionCoordinates
105 variable {I S : Type*} [Fintype I] [Nonempty I]
106 
107 /-- P26's coordinate realization, including the first row, onto property,
108 exact row space and uniqueness. No supplied reduced operator is assumed. -/
109 theorem finite_instrument_coordinates
110     (L : S → (I → ℝ) →ₗ[ℝ] (I → ℝ)) :
111     ∃ (r : ℕ) (hr : 0 < r)
112       (R : (I → ℝ) →ₗ[ℝ] (Fin r → ℝ))
113       (B : S → (Fin r → ℝ) →ₗ[ℝ] (Fin r → ℝ)),
114       r = finrank ℝ (instrumentCompletion L mass) ∧
115       LinearIndependent ℝ (fun j => (LinearMap.proj j).comp R) ∧
116       Function.Surjective R ∧
117       LinearMap.range R.dualMap = instrumentCompletion L mass ∧
118       (LinearMap.proj ⟨0,hr⟩).comp R = mass ∧
119       (∀ s, (B s).comp R = R.comp (L s)) ∧
120       (∀ s D, D.comp R = R.comp (L s) → D = B s) := by
121   classical
122   let W := instrumentCompletion L (mass : (I → ℝ) →ₗ[ℝ] ℝ)
123   let w : W := ⟨mass, massRow_mem_completion L mass⟩
124   have hw : w ≠ 0 := by
125     intro h
126     exact mass_ne_zero (congrArg (fun x : W => (x : Dual ℝ (I → ℝ))) h)
127   obtain ⟨r,hr,b,hb⟩ := exists_basis_first w hw
128   have hW := instrumentCompletion_invariant L (mass : (I → ℝ) →ₗ[ℝ] ℝ)
129   refine ⟨r,hr,basisObservation b,basisTransition L hW b, ?_,
130     basisObservation_independent b,basis_observation_surjective b,
131     basis_observation_rowspace b, ?_,basisTransition_correct L hW b, ?_⟩
132   · simpa only [Fintype.card_fin] using (Module.finrank_eq_card_basis b).symm
133   · apply LinearMap.ext
134     intro p
135     change (b ⟨0,hr⟩ : Dual ℝ (I → ℝ)) p = mass p
136     rw [hb]
137   · intro s D hD
138     exact closed_operator_unique (basisObservation b) (basis_observation_surjective b)
139       (L s) (basisTransition L hW b s) D (basisTransition_correct L hW b s) hD
140 
141 end CompletionCoordinates
142 end Komorebi.LSM.FiniteInstruments

Back to source controls