TransferLearningCertificate.lean

1 import KomorebiLSM.EllipsoidDiscoveryP63
2 import KomorebiLSM.BernsteinCoefficientError
3 import KomorebiLSM.PredictableResidualP66
4 import KomorebiLSM.CoveredAdaptiveEvidence
5 import KomorebiLSM.ObservationLawComparison
6 
7 /-! P70 composition. Structural replay, common-domain approximation, external
8 causal comparison and actual sequential evidence retain their own assumptions.
9 The new bridges below derive full-law upper and simultaneous lower certificates;
10 neither structural acceptance nor nonrejection is an accuracy assumption. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.TransferLearningCertificate
13 open MeasureTheory ProbabilityTheory
14 open scoped BigOperators NNReal ENNReal
15 
16 section Structure
17 variable {D A : Type*} [Fintype D] [DecidableEq D]
18 variable [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
19 
20 /-- The structural part of P70 is obtained from a literal finite P62 certificate,
21 including exact integrated mass and a normalized initial state. No successful
22 geometry-discovery proposal is required. -/
23 theorem structural_acceptance (c : D → ℝ) (H : Matrix D D ℝ) (hH : H.PosDef)
24     {n q bound : ℕ} (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
25     (cert : OrientedEllipsoid.PolynomialCertificate c H B q bound)
26     (z : OrientedEllipsoid.State D) (hz : z∈OrientedEllipsoid.cone c H)
27     (hm : OrientedEllipsoid.mass z=1) :
28     (∀ word : List (A × ℝ),(∀ s∈word,s.2∈Set.Icc (-1:ℝ) 1) →
29       0≤OrientedEllipsoid.mass (FiniteInstruments.wordAction
30         (fun s : A × ℝ => (OrientedEllipsoid.polynomialOperator (B s.1) s.2).toLinearMap) word z)) ∧
31     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T,
32       IsProbabilityMeasure (ContinuousRecords.recordLaw (cert.instrument hH) π z T)) ∧
33     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T extra,
34       (ContinuousRecords.recordLaw (cert.instrument hH) π z (T+extra)).map
35         (ContinuousRecords.truncate T extra)=ContinuousRecords.recordLaw (cert.instrument hH) π z T) := by
36   exact ⟨fun word hword => cert.word_mass_nonneg hH word hword hz,
37     fun π T => cert.record_law_probability hH π z hz hm T,
38     fun π T extra => cert.record_law_prefix hH π z hz T extra⟩
39 end Structure
40 
41 section Approximation
42 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
43 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
44 variable [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
45 variable (C : BaseNorm.ProbabilityCone E)
46 
47 /-- Finite positive coefficient budgets and a genuine Lipschitz hypothesis give
48 an upper bound for the actual complete joint laws of the true density and its
49 fitted polynomial model. The common cone, reference and policy are explicit. -/
50 theorem common_domain_upper_law (n : ℕ)
51     (D : ContinuousInstrument.DensityInstrument (A := A) C BernsteinKernel.measure)
52     (T : A → Fin (n+1) → E →L[ℝ] E) (eta : A → Fin (n+1) → ℝ)
53     (hT : ∀ a k z,z∈C.carrier → T a k z∈C.carrier)
54     (hm : ∀ a z,C.mass (((1/((n:ℝ)+1)) • ∑ k,T a k) z)=C.mass z)
55     (L : ℝ) (hL : 0≤L)
56     (hLip : ∀ a x,x∈Set.Icc (0:ℝ) 1 → ∀ v∈Set.Icc (0:ℝ) 1,
57       PositiveCellApproximation.inducedNorm (C := C) (D.op a v-D.op a x)≤L*|v-x|)
58     (herror : ∀ a k z,z∈C.base →
59       C.value (PositivePolynomialApproximation.coefficient n (D.op a) k z-T a k z)≤eta a k)
60     (π : ContinuousRecords.Policy (A := A) (Y := ℝ))
61     (z : ContinuousInstrument.DensityInstrument.State C) (horizon : ℕ) :
62     SequentialLowerCertificate.lawTV (TimeRecords.recordLaw (fun _ => D) π z.1 horizon)
63       (TimeRecords.recordLaw (fun _ => BernsteinCoefficientError.fittedInstrument C n T hT hm)
64         π z.1 horizon)≤
65       min 1 ((horizon:ℝ)/2*(L/Real.sqrt (3*((n:ℝ)+2))+
66         BernsteinCoefficientError.maximumCoefficientError n eta)) := by
67   let F := BernsteinCoefficientError.fittedInstrument C n T hT hm
68   let ε := L/Real.sqrt (3*((n:ℝ)+2))+
69     BernsteinCoefficientError.maximumCoefficientError n eta
70   have heta (a : A) (k : Fin (n+1)) : 0≤eta a k :=
71     (C.value_nonneg _).trans (herror a k z.1 z.2)
72   have hε : 0≤ε := by
73     have hA : Nonempty A := by
74       by_contra h
75       let : IsEmpty A := ⟨fun a => h ⟨a⟩⟩
76       have hh := π.sum_one 0 PUnit.unit
77       simp at hh
78     have hcoef : 0≤BernsteinCoefficientError.maximumCoefficientError n eta :=
79       (mul_nonneg (by positivity : 0≤1/((n:ℝ)+1))
80         (Finset.sum_nonneg (fun k _ => heta (Classical.choice hA) k))).trans
81           (BernsteinCoefficientError.coefficient_error_le_maximum n eta (Classical.choice hA))
82     exact add_nonneg (div_nonneg hL (Real.sqrt_nonneg _)) hcoef
83   have h := ContinuousTV.record_lawTV_le (fun _ => D) (fun _ => F) π z z (fun _ => ε)
84     (fun _ => hε)
85     (fun _ a u hu => BernsteinCoefficientError.uniform_bias_plus_coefficient_error
86       C n D T eta L hL hLip herror a u hu)
87     0 (by simp) horizon
88   convert h using 1
89   congr 1
90   simp only [Finset.sum_const,Finset.card_range,nsmul_eq_mul,zero_add]
91   dsimp only [ε]
92   ring
93 end Approximation
94 
95 section Evidence
96 variable {Ω J Y : Type*} [mΩ : MeasurableSpace Ω] [MeasurableSpace Y] [Countable J]
97 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
98 
99 omit [IsProbabilityMeasure μ] in
100 /-- A measurable high-probability event can be refined by an AE implication
101 without requiring the target predicate itself to be measurable. The returned
102 set remains measurable and has exactly the same probability as the original. -/
103 theorem refine_event_ae (E : Set Ω) (hE : MeasurableSet E) (P : Ω → Prop)
104     (hP : ∀ᵐ ω∂μ,ω∈E → P ω) :
105     ∃ G : Set Ω,MeasurableSet G ∧ G⊆E ∧ μ G=μ E ∧ ∀ ω∈G,P ω := by
106   have hbad : μ {ω | ¬(ω∈E → P ω)}=0 := ae_iff.mp hP
107   obtain ⟨N,hsub,hN,hnull⟩ := exists_measurable_superset_of_null hbad
108   have hNae : ∀ᵐ ω∂μ,ω∉N := by
109     apply ae_iff.mpr
110     simpa using hnull
111   refine ⟨E\N,hE.diff hN,Set.sdiff_subset,?_,?_⟩
112   · apply measure_congr
113     filter_upwards [hNae] with ω hω
114     simp only [Set.mem_sdiff,hω,not_false_eq_true,and_true]
115   · intro ω hω
116     by_contra hnot
117     exact hω.2 (hsub (by exact fun hp => hnot (hp hω.1)))
118 
119 /-- Full P66 implies simultaneous P68 lower certificates for the actual true
120 and proposed observation laws, when the true bounded-test means are the actual
121 conditional expectations. The returned event is genuinely measurable, includes
122 all registered rules and all positive times, and retains probability 1-delta. -/
123 theorem simultaneous_lower_evidence (ℱ : Filtration ℕ mΩ) (X : J → ℕ → Ω → ℝ)
124     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i))
125     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (0:ℝ) 1)
126     (P Q : J → ℕ → Ω → Measure Y)
127     [∀ j i ω,IsProbabilityMeasure (P j i ω)] [∀ j i ω,IsProbabilityMeasure (Q j i ω)]
128     (φ : J → ℕ → Ω → Y → ℝ)
129     (hφ : ∀ j i ω,Measurable (φ j i ω))
130     (hφ0 : ∀ j i ω y,0≤φ j i ω y) (hφ1 : ∀ j i ω y,φ j i ω y≤1)
131     (htrue : ∀ j i,(μ[X j i | ℱ i])=ᵐ[μ] (fun ω => ∫ y,φ j i ω y∂P j i ω))
132     (α : J → NNReal) (hα : ∀ j,0<α j) (hs : Summable α)
133     (δ : NNReal) (hbudget : ∑' j,α j≤δ) (hδ1 : δ≤1) :
134     ∃ good : Set Ω,MeasurableSet good ∧ 1-(δ:ℝ)≤μ.real good ∧
135       ∀ ω∈good,∀ j t,0<t →
136         max (|SequentialLowerCertificate.residual t (fun i => X j i ω)
137           (fun i => ∫ y,φ j i ω y∂Q j i ω)|-PredictableResidual.boundary t (α j)) 0/(t:ℝ)≤
138         (∑ i∈Finset.range t,SequentialLowerCertificate.lawTV (P j i ω) (Q j i ω))/(t:ℝ) := by
139   let p : J → ℕ → Ω → ℝ := fun j i ω => ∫ y,φ j i ω y∂Q j i ω
140   let E : Set Ω := {ω | ∀ j n,
141     |PredictableResidual.observedResidual (X j) (p j) (n+1) ω-
142       PredictableResidual.conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤
143         PredictableResidual.boundary (n+1) (α j)}
144   have hEm : MeasurableSet E := by
145     simpa only [E,PredictableResidual.residual_sub_drift] using
146       PredictableResidualGeneral.unit_event_measurable ℱ X hX α
147   have hprob : 1-(δ:ℝ)≤μ.real E :=
148     PredictableResidualGeneral.predictable_residual_certificate_countable ℱ X p hX hb α hα hs δ hbudget hδ1
149   have hmeans : ∀ᵐ ω∂μ,∀ j i,(μ[X j i | ℱ i]) ω=∫ y,φ j i ω y∂P j i ω :=
150     ae_all_iff.mpr (fun j => ae_all_iff.mpr (fun i => htrue j i))
151   have hpoint : ∀ᵐ ω∂μ,ω∈E → ∀ j t,0<t →
152       max (|SequentialLowerCertificate.residual t (fun i => X j i ω)
153         (fun i => ∫ y,φ j i ω y∂Q j i ω)|-PredictableResidual.boundary t (α j)) 0/(t:ℝ)≤
154       (∑ i∈Finset.range t,SequentialLowerCertificate.lawTV (P j i ω) (Q j i ω))/(t:ℝ) := by
155     filter_upwards [hmeans] with ω hmeans hall
156     intro j t ht
157     apply SequentialLowerCertificate.sequential_lower_certificate t ht
158       (fun i => P j i ω) (fun i => Q j i ω) (fun i => φ j i ω) (fun i => X j i ω)
159       (PredictableResidual.boundary t (α j)) (fun i => hφ j i ω)
160       (fun i => hφ0 j i ω) (fun i => hφ1 j i ω)
161     have htime : (t-1)+1=t := by omega
162     have he := hall j (t-1)
163     rw [htime] at he
164     have hsum : SequentialLowerCertificate.drift t (fun i => ∫ y,φ j i ω y∂P j i ω)
165         (fun i => ∫ y,φ j i ω y∂Q j i ω)=
166         PredictableResidual.conditionalDrift (μ:=μ) ℱ (X j) (p j) t ω := by
167       apply Finset.sum_congr rfl
168       intro i _
169       rw [hmeans j i]
170     rw [hsum]
171     exact he
172   obtain ⟨G,hG,hGE,hμG,hgood⟩ := refine_event_ae E hEm _ hpoint
173   exact ⟨G,hG,by simpa only [Measure.real,hμG] using hprob,hgood⟩
174 end Evidence
175 
176 end Komorebi.LSM.TransferLearningCertificate

Back to source controls