ObservableMomentConfidence.lean

1 import KomorebiLSM.ObservableOperatorSets
2 import KomorebiLSM.RegressionConfidence
3 import KomorebiLSM.CountableConfidence
4 
5 /-! Full P82 confidence transfer from actual rowwise P81 regression events.
6 Rows and moments share observations freely; only the literal finite prospective
7 budget is added. Exact mass intersection preserves the true coefficients. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.ObservableMoments
10 open MeasureTheory ProbabilityTheory Matrix RegressionConfidence
11 open scoped BigOperators NNReal Matrix
12 
13 variable {Ω H A Y : Type*} {p r : ℕ} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
14 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
15 variable {C : BaseNorm.ProbabilityCone (Fin r → ℝ)} {ν : Measure Y} [IsProbabilityMeasure ν]
16 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
17 variable {μ : Measure Ω} [IsProbabilityMeasure μ] {ℱ : Filtration ℕ mΩ}
18 variable (P : AccessibleProcess (H := H) (μ := μ) D ℱ)
19 
20 abbrev RowIndex (A : Type*) (p r : ℕ) := A × Fin p × Fin r
21 
22 noncomputable def rowParameter (g : Fin p → Y → ℝ) (k : RowIndex A p r) : Fin r → ℝ :=
23   fun l => momentMatrix D (g k.2.1) k.1 k.2.2 l
24 
25 /-- Every fitted row is the literal ridge estimator from the recorded
26 action-gated design and recorded accessible-state response. -/
27 noncomputable def fittedMomentMatrices (γ : A → ℝ) (g : Fin p → Y → ℝ)
28     (n : ℕ) (ω : Ω) : CoefficientFamily A p r := fun a j i =>
29   ridgeEstimate (γ a) (fun s => gatedDesign D P a s ω)
30     (fun s => gatedResponse D P a (g j) i s ω) n
31 
32 noncomputable def actionDesign (γ : A → ℝ) (n : ℕ) (ω : Ω) : A → Matrix (Fin r) (Fin r) ℝ :=
33   fun a => ridgeMatrix (γ a) (fun s => gatedDesign D P a s ω) n
34 
35 noncomputable def momentRadius (γ : A → ℝ) (σ S : RowIndex A p r → ℝ)
36     (α : RowIndex A p r → NNReal) (n : ℕ) (ω : Ω) : A → Fin p → Fin r → ℝ :=
37   fun a j i => noiseRadius (γ a) (σ (a,j,i)) (α (a,j,i))
38     (fun s => gatedDesign D P a s ω) n+Real.sqrt (γ a)*S (a,j,i)
39 
40 noncomputable def rowGoodEvent (γ : A → ℝ) (σ : RowIndex A p r → ℝ)
41     (α : RowIndex A p r → NNReal) (g : Fin p → Y → ℝ) (k : RowIndex A p r) : Set Ω :=
42   regressionGood (γ k.1) (σ k) (α k) (gatedDesign D P k.1)
43     (gatedResponse D P k.1 (g k.2.1) k.2.2) (rowParameter D g k)
44 
45 /-- A literal finite intersection of the actual Gaussian-mixture P81 events. -/
46 noncomputable def operatorGoodEvent (γ : A → ℝ) (σ : RowIndex A p r → ℝ)
47     (α : RowIndex A p r → NNReal) (g : Fin p → Y → ℝ) : Set Ω :=
48   ⋂ k : RowIndex A p r,rowGoodEvent D P γ σ α g k
49 
50 /-- Full row coverage is derived by applying P81 to every actual moment row
51 and then the finite prospective union bound. No independence between rows is
52 assumed, and no row-confidence event is supplied as a certificate field. -/
53 theorem moment_row_confidence (γ : A → ℝ) (hγ : ∀ a,0<γ a)
54     (σ S : RowIndex A p r → ℝ) (hσ : ∀ k,0<σ k)
55     (α : RowIndex A p r → NNReal) (hα : ∀ k,0<α k)
56     (δ : NNReal) (hbudget : ∑ k,α k≤δ)
57     (g : Fin p → Y → ℝ) (hg : ∀ j,Measurable (g j))
58     (hθ : ∀ k,euclideanNorm (rowParameter D g k)≤S k)
59     (Hnoise : ∀ k n,ConditionalSubgaussian (ℱ.le n)
60       (regressionNoise (rowParameter D g k) (gatedDesign D P k.1)
61         (gatedResponse D P k.1 (g k.2.1) k.2.2) n) (σ k) μ) :
62     MeasurableSet (operatorGoodEvent D P γ σ α g) ∧
63     1-(δ:ℝ)≤μ.real (operatorGoodEvent D P γ σ α g) ∧
64     ∀ ω∈operatorGoodEvent D P γ σ α g,∀ n a j i,
65       weightedNorm (actionDesign D P γ n ω a)
66         (fun l => fittedMomentMatrices D P γ g n ω a j i l-momentMatrix D (g j) a i l)≤
67           momentRadius D P γ σ S α n ω a j i := by
68   classical
69   have hc (k : RowIndex A p r) := regression_confidence_certificate (μ := μ) ℱ
70     (γ k.1) (σ k) (α k) (S k) (hγ k.1) (hσ k) (by exact_mod_cast hα k)
71     (gatedDesign D P k.1) (gatedResponse D P k.1 (g k.2.1) k.2.2) (rowParameter D g k)
72     (fun n i => (measurable_pi_apply i).comp (gatedDesign_measurable D P k.1 n))
73     (gatedResponse_measurable D P k.1 (g k.2.1) (hg k.2.1) k.2.2)
74     (hθ k) (Hnoise k)
75   refine ⟨?_,?_,?_⟩
76   · exact MeasurableSet.iInter (fun k => (hc k).1)
77   · have hb (k : RowIndex A p r) : μ.real (rowGoodEvent D P γ σ α g k)ᶜ≤(α k:ℝ) := by
78       unfold rowGoodEvent
79       rw [measureReal_compl (hc k).1,probReal_univ]
80       linarith [(hc k).2.1]
81     have hu := CountableConfidence.finite_simultaneous_coverage
82       (fun k => (rowGoodEvent D P γ σ α g k)ᶜ) (fun k => (hc k).1.compl)
83       α δ hbudget hb
84     simpa only [compl_compl,operatorGoodEvent] using hu
85   · intro ω hω n a j i
86     have hr := (hc (a,j,i)).2.2 ω (Set.mem_iInter.mp hω (a,j,i)) n
87     change weightedNorm (ridgeMatrix (γ a) (fun s => gatedDesign D P a s ω) n)
88       (ridgeEstimate (γ a) (fun s => gatedDesign D P a s ω)
89         (fun s => gatedResponse D P a (g j) i s ω) n-rowParameter D g (a,j,i))≤
90       noiseRadius (γ a) (σ (a,j,i)) (α (a,j,i))
91         (fun s => gatedDesign D P a s ω) n+Real.sqrt (γ a)*S (a,j,i)
92     exact hr
93 
94 /-- The submitted coefficient estimate is the known inverse moment map of
95 the actual fitted row-regression matrices. -/
96 noncomputable def coefficientEstimate (W : Matrix (Fin p) (Fin p) ℝ) (γ : A → ℝ)
97     (g : Fin p → Y → ℝ) (n : ℕ) (ω : Ω) : CoefficientFamily A p r :=
98   fun a => FiniteMomentIdentification.mix W⁻¹ (fittedMomentMatrices D P γ g n ω a)
99 
100 /-- Full P82: actual conditional moment semantics and known basis inversion
101 are combined with the actual finite-family P81 event. On that one measurable
102 event, every finite-time coefficient set contains the true coefficients after
103 exact mass intersection, and every directional row bound is genuine. -/
104 theorem observable_moment_operator_confidence
105     (B : A → Fin p → (Fin r → ℝ) →L[ℝ] (Fin r → ℝ))
106     (g ψ : Fin p → Y → ℝ) (hg : ∀ j,Measurable (g j))
107     (hB : ∀ a y,D.op a y=∑ k,ψ k y • B a k)
108     (hgψ : ∀ j k,Integrable (fun y => g j y*ψ k y) ν) (hψ : ∀ k,Integrable (ψ k) ν)
109     (hW : IsUnit (basisMomentMatrix (ν := ν) g ψ))
110     (γ : A → ℝ) (hγ : ∀ a,0<γ a)
111     (σ S : RowIndex A p r → ℝ) (hσ : ∀ k,0<σ k)
112     (α : RowIndex A p r → NNReal) (hα : ∀ k,0<α k)
113     (δ : NNReal) (hbudget : ∑ k,α k≤δ)
114     (hθ : ∀ k,euclideanNorm (rowParameter D g k)≤S k)
115     (Hnoise : ∀ k n,ConditionalSubgaussian (ℱ.le n)
116       (regressionNoise (rowParameter D g k) (gatedDesign D P k.1)
117         (gatedResponse D P k.1 (g k.2.1) k.2.2) n) (σ k) μ) :
118     (∀ j n,μ[fun ω => g j (P.observation n ω) • currentState D P (n+1) ω | ℱ n]=ᵐ[μ]
119       (fun ω => momentOperator D (g j) (currentAction D P n ω) (currentState D P n ω))) ∧
120     (∀ a j i n,μ[gatedResponse D P a (g j) i n | ℱ n]=ᵐ[μ]
121       (fun ω => (momentMatrix D (g j) a *ᵥ gatedDesign D P a n ω) i)) ∧
122     (∀ a,coefficientMatrices B a=FiniteMomentIdentification.mix
123       (basisMomentMatrix (ν := ν) g ψ)⁻¹ (fun j => momentMatrix D (g j) a)) ∧
124     MeasurableSet (operatorGoodEvent D P γ σ α g) ∧
125     1-(δ:ℝ)≤μ.real (operatorGoodEvent D P γ σ α g) ∧
126     (∀ ω∈operatorGoodEvent D P γ σ α g,∀ n,
127       coefficientMatrices B∈massConstrainedRegion (basisMomentMatrix (ν := ν) g ψ)
128         (fittedMomentMatrices D P γ g n ω) (actionDesign D P γ n ω)
129         (momentRadius D P γ σ S α n ω) C.mass (basisIntegral (ν := ν) ψ) ∧
130       ∀ a k i x,
131         |(coefficientEstimate D P (basisMomentMatrix (ν := ν) g ψ) γ g n ω a k *ᵥ x) i-
132           (coefficientMatrices B a k *ᵥ x) i|≤
133           ∑ j,|(basisMomentMatrix (ν := ν) g ψ)⁻¹ k j| * momentRadius D P γ σ S α n ω a j i *
134             weightedNorm (actionDesign D P γ n ω a)⁻¹ x) := by
135   have hi (j : Fin p) (a : A) : Integrable (fun y => g j y • D.op a y) ν :=
136     weighted_operator_integrable D B ψ hB (g j) (hgψ j) a
137   obtain ⟨hG,hprob,hrows⟩ := moment_row_confidence D P γ hγ σ S hσ α hα δ hbudget g hg hθ Hnoise
138   refine ⟨?_,?_,matrix_coefficient_reconstruction D B g ψ hB hgψ hW,hG,hprob,?_⟩
139   · intro j n
140     exact process_conditional_moment D P (g j) (hg j) (hi j) n
141   · intro a j i n
142     exact gatedResponse_condExp D P a (g j) (hg j) (hi j) i n
143   · intro ω hω n
144     have hr := hrows ω hω n
145     have htrue := true_coefficients_in_mass_region D B g ψ hB hgψ hψ hW
146       (fittedMomentMatrices D P γ g n ω) (actionDesign D P γ n ω)
147       (momentRadius D P γ σ S α n ω) hr
148     refine ⟨htrue,?_⟩
149     exact coefficient_region_directional _ _ _
150       (fun a => ridgeMatrix_posDef (γ a) (hγ a) (fun s => gatedDesign D P a s ω) n)
151       _ htrue.1
152 
153 end Komorebi.LSM.ObservableMoments

Back to source controls