ObservableOperatorSets.lean

1 import KomorebiLSM.ObservableMomentAlgebra
2 import KomorebiLSM.ObservableMomentProcess
3 
4 /-! Known linear moment inversion defines actual coefficient confidence sets.
5 Exact integrated mass is imposed only by its literal affine constraints. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ObservableMoments
8 open MeasureTheory Matrix FiniteMomentIdentification
9 open scoped BigOperators Matrix
10 
11 section Matrices
12 variable {p r : ℕ}
13 
14 noncomputable def operatorMatrix (L : (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) :
15     Matrix (Fin r) (Fin r) ℝ := LinearMap.toMatrix' L.toLinearMap
16 
17 @[simp] theorem operatorMatrix_mulVec (L : (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) (z : Fin r → ℝ) :
18     operatorMatrix L *ᵥ z=L z := LinearMap.toMatrix'_mulVec _ _
19 
20 theorem operatorMatrix_sum (B : Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) (w : Fin p → ℝ) :
21     operatorMatrix (∑ k,w k • B k)=∑ k,w k • operatorMatrix (B k) := by
22   unfold operatorMatrix
23   simp only [ContinuousLinearMap.toLinearMap_sum,ContinuousLinearMap.toLinearMap_smul,map_sum,map_smul]
24 
25 end Matrices
26 
27 section ActualCoefficients
28 variable {A Y : Type*} {p r : ℕ} [MeasurableSpace Y]
29 variable {C : BaseNorm.ProbabilityCone (Fin r → ℝ)} {ν : Measure Y}
30 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
31 
32 /-- The actual coefficient matrices of the submitted operator density. -/
33 noncomputable def coefficientMatrices
34     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) :
35     A → Fin p → Matrix (Fin r) (Fin r) ℝ := fun a k => operatorMatrix (B a k)
36 
37 /-- Actual observation-basis integration commutes with the fixed coordinate
38 matrix representation used by the row regressions. -/
39 theorem matrix_moment_mixing (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ))
40     (g ψ : Fin p → Y → ℝ) (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
41     (hgψ : ∀ j k,Integrable (fun y => g j y*ψ k y) ν) (a : A) :
42     (fun j => momentMatrix D (g j) a)=
43       mix (basisMomentMatrix (ν := ν) g ψ) (coefficientMatrices B a) := by
44   funext j
45   change operatorMatrix (momentOperator D (g j) a)=_
46   rw [congrFun (momentOperator_mixing D B g ψ hB hgψ a) j]
47   exact operatorMatrix_sum _ _
48 
49 /-- Literal true coefficients, rather than arbitrary target matrices, are
50 reconstructed from the actual instrument moment matrices. -/
51 theorem matrix_coefficient_reconstruction
52     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ))
53     (g ψ : Fin p → Y → ℝ) (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
54     (hgψ : ∀ j k,Integrable (fun y => g j y*ψ k y) ν)
55     (hW : IsUnit (basisMomentMatrix (ν := ν) g ψ)) (a : A) :
56     coefficientMatrices B a=
57       mix (basisMomentMatrix (ν := ν) g ψ)⁻¹ (fun j => momentMatrix D (g j) a) := by
58   rw [matrix_moment_mixing D B g ψ hB hgψ a,inverse_mix _ hW]
59 
60 noncomputable def basisIntegral (ψ : Fin p → Y → ℝ) (k : Fin p) : ℝ := ∫ y,ψ k y∂ν
61 
62 theorem integratedOperator_expansion
63     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) (ψ : Fin p → Y → ℝ)
64     (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
65     (hψ : ∀ k,Integrable (ψ k) ν) (a : A) :
66     (∫ y,D.op a y∂ν)=∑ k,basisIntegral (ν := ν) ψ k • B a k := by
67   simp_rw [hB]
68   rw [integral_finsetSum _ (fun k _ => (hψ k).smul_const (B a k))]
69   apply Finset.sum_congr rfl
70   intro k _
71   exact integral_smul_const _ _
72 
73 end ActualCoefficients
74 
75 section Sets
76 variable {A : Type*} {p r : ℕ}
77 abbrev CoefficientFamily (A : Type*) (p r : ℕ) := A → Fin p → Matrix (Fin r) (Fin r) ℝ
78 
79 /-- The row ellipsoids are defined using the actual positive-definite design
80 matrix norm, not entrywise or Euclidean surrogate errors. -/
81 def momentRegion (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
82     (β : A → Fin p → Fin r → ℝ) : Set (CoefficientFamily A p r) :=
83   {M | ∀ a j i,RegressionConfidence.weightedNorm (V a) (fun l => Mhat a j i l-M a j i l)≤β a j i}
84 
85 /-- The known inverse integration map gives the coefficient set exactly. -/
86 def coefficientRegion (W : Matrix (Fin p) (Fin p) ℝ) (Mhat : CoefficientFamily A p r)
87     (V : A → Matrix (Fin r) (Fin r) ℝ) (β : A → Fin p → Fin r → ℝ) :
88     Set (CoefficientFamily A p r) :=
89   {F | ∃ M∈momentRegion Mhat V β,∀ a,F a=mix W⁻¹ (M a)}
90 
91 /-- Invertibility makes coefficient-set membership exactly a row-ellipsoid
92 condition on the known forward moment map. No arbitrary projection event is
93 substituted for the actual confidence event. -/
94 theorem coefficientRegion_iff (W : Matrix (Fin p) (Fin p) ℝ) (hW : IsUnit W)
95     (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
96     (β : A → Fin p → Fin r → ℝ) (F : CoefficientFamily A p r) :
97     F∈coefficientRegion W Mhat V β ↔ (fun a => mix W (F a))∈momentRegion Mhat V β := by
98   constructor
99   · rintro ⟨M,hM,hF⟩
100     have he (a : A) : mix W (F a)=M a := by
101       rw [hF a,mix_mul,Matrix.mul_nonsing_inv W ((Matrix.isUnit_iff_isUnit_det W).mp hW),mix_one]
102     simpa only [he] using hM
103   · intro hM
104     exact ⟨(fun a => mix W (F a)),hM,fun a => (inverse_mix W hW (F a)).symm⟩
105 
106 /-- Every integrated mass constraint is a real linear map of the submitted
107 coefficient array, with the known basis integrals kept explicit. -/
108 noncomputable def massConstraint (l : (Fin r → ℝ) →ₗ[ℝ] ℝ) (η : Fin p → ℝ)
109     (a : A) (z : Fin r → ℝ) : CoefficientFamily A p r →ₗ[ℝ] ℝ where
110   toFun F := l ((∑ k,η k • F a k) *ᵥ z)
111   map_add' F G := by
112     simp only [Pi.add_apply,smul_add,Finset.sum_add_distrib,Matrix.add_mulVec,map_add]
113   map_smul' c F := by
114     have he : (∑ k,η k • (c • F a k))=c • ∑ k,η k • F a k := by
115       simp only [Finset.smul_sum,smul_smul]
116       apply Finset.sum_congr rfl
117       intro k _
118       rw [mul_comm]
119     change l ((∑ k,η k • (c • F a k)) *ᵥ z)=c*l ((∑ k,η k • F a k) *ᵥ z)
120     rw [he,Matrix.smul_mulVec,map_smul]
121     rfl
122 
123 /-- Literal integrated mass, an affine slice independent of the data. -/
124 def exactMassRegion (l : (Fin r → ℝ) →ₗ[ℝ] ℝ) (η : Fin p → ℝ) :
125     Set (CoefficientFamily A p r) := {F | ∀ a z,massConstraint l η a z F=l z}
126 
127 def massConstrainedRegion (W : Matrix (Fin p) (Fin p) ℝ)
128     (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
129     (β : A → Fin p → Fin r → ℝ) (l : (Fin r → ℝ) →ₗ[ℝ] ℝ) (η : Fin p → ℝ) :
130     Set (CoefficientFamily A p r) := coefficientRegion W Mhat V β ∩ exactMassRegion l η
131 
132 /-- Every coefficient candidate inherits the genuine directional row bound
133 from a moment ellipsoid through the known inverse map. -/
134 theorem coefficient_region_directional (W : Matrix (Fin p) (Fin p) ℝ)
135     (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
136     (hV : ∀ a,(V a).PosDef) (β : A → Fin p → Fin r → ℝ)
137     {F : CoefficientFamily A p r} (hF : F∈coefficientRegion W Mhat V β)
138     (a : A) (k : Fin p) (i : Fin r) (x : Fin r → ℝ) :
139     |(mix W⁻¹ (Mhat a) k *ᵥ x) i-(F a k *ᵥ x) i|≤
140       ∑ j,|W⁻¹ k j| * β a j i*RegressionConfidence.weightedNorm (V a)⁻¹ x := by
141   obtain ⟨M,hM,hFM⟩ := hF
142   rw [hFM a]
143   exact mixed_directional_error W⁻¹ (Mhat a) (M a) (V a) (hV a) (β a) (hM a) k i x
144 
145 end Sets
146 
147 section Truth
148 variable {A Y : Type*} {p r : ℕ} [MeasurableSpace Y]
149 variable {C : BaseNorm.ProbabilityCone (Fin r → ℝ)} {ν : Measure Y}
150 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
151 
152 /-- The actual instrument's mass law places the true coefficient family in
153 the exact affine slice; entrywise confidence bounds play no role here. -/
154 theorem true_coefficients_exact_mass
155     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ)) (ψ : Fin p → Y → ℝ)
156     (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k) (hψ : ∀ k,Integrable (ψ k) ν) :
157     coefficientMatrices B∈exactMassRegion C.mass (basisIntegral (ν := ν) ψ) := by
158   intro a z
159   change C.mass ((∑ k,basisIntegral (ν := ν) ψ k • operatorMatrix (B a k)) *ᵥ z)=C.mass z
160   rw [← operatorMatrix_sum,operatorMatrix_mulVec,← integratedOperator_expansion D B ψ hB hψ a]
161   exact D.mass_preserving a z
162 
163 /-- Exact mass intersection preserves inclusion of the literal true
164 coefficients whenever the actual moment rows obey their confidence bounds. -/
165 theorem true_coefficients_in_mass_region
166     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ))
167     (g ψ : Fin p → Y → ℝ) (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
168     (hgψ : ∀ j k,Integrable (fun y => g j y*ψ k y) ν) (hψ : ∀ k,Integrable (ψ k) ν)
169     (hW : IsUnit (basisMomentMatrix (ν := ν) g ψ))
170     (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
171     (β : A → Fin p → Fin r → ℝ)
172     (hb : ∀ a j i,RegressionConfidence.weightedNorm (V a)
173       (fun l => Mhat a j i l-momentMatrix D (g j) a i l)≤β a j i) :
174     coefficientMatrices B∈massConstrainedRegion (basisMomentMatrix (ν := ν) g ψ)
175       Mhat V β C.mass (basisIntegral (ν := ν) ψ) := by
176   constructor
177   · exact ⟨(fun a j => momentMatrix D (g j) a),hb,
178       matrix_coefficient_reconstruction D B g ψ hB hgψ hW⟩
179   · exact true_coefficients_exact_mass D B ψ hB hψ
180 
181 /-- The literal true-coefficient coverage event is exactly the actual moment
182 row confidence event. Intersecting exact mass costs no probability, because
183 the real instrument supplies that mass law. -/
184 theorem true_mass_region_iff
185     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ))
186     (g ψ : Fin p → Y → ℝ) (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
187     (hgψ : ∀ j k,Integrable (fun y => g j y*ψ k y) ν) (hψ : ∀ k,Integrable (ψ k) ν)
188     (hW : IsUnit (basisMomentMatrix (ν := ν) g ψ))
189     (Mhat : CoefficientFamily A p r) (V : A → Matrix (Fin r) (Fin r) ℝ)
190     (β : A → Fin p → Fin r → ℝ) :
191     coefficientMatrices B∈massConstrainedRegion (basisMomentMatrix (ν := ν) g ψ)
192       Mhat V β C.mass (basisIntegral (ν := ν) ψ) ↔
193     ∀ a j i,RegressionConfidence.weightedNorm (V a)
194       (fun l => Mhat a j i l-momentMatrix D (g j) a i l)≤β a j i := by
195   change (coefficientMatrices B∈coefficientRegion (basisMomentMatrix (ν := ν) g ψ) Mhat V β ∧
196     coefficientMatrices B∈exactMassRegion C.mass (basisIntegral (ν := ν) ψ)) ↔ _
197   rw [and_iff_left (true_coefficients_exact_mass D B ψ hB hψ),
198     coefficientRegion_iff _ hW]
199   have he : (fun a => mix (basisMomentMatrix (ν := ν) g ψ) (coefficientMatrices B a))=
200       (fun a j => momentMatrix D (g j) a) := by
201     funext a
202     exact (matrix_moment_mixing D B g ψ hB hgψ a).symm
203   rw [he]
204   rfl
205 
206 end Truth
207 end Komorebi.LSM.ObservableMoments

Back to source controls