CertifiedCorrection.lean

1 import KomorebiLSM.RobustFiniteDomains
2 import Mathlib.Analysis.Normed.Group.Basic
3 
4 /-! P41: a feasible finite witness, statistical set membership, and correction
5 error are separate conditions. No true-domain coverage is inferred from feasibility. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.CertifiedCorrection
8 open scoped BigOperators
9 open FiniteInstruments PositiveLift
10 variable {E A O J : Type*} [AddCommGroup E] [Module ℝ E] [Fintype O] [Fintype J]
11 
12 /-- These are finite feasibility constraints, not assumed future probabilities. -/
13 structure FeasiblePoint (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) where
14   family : A × O → E →ₗ[ℝ] E
15   lift : A × O → Matrix J J ℝ
16   nonneg : ∀ s i j, 0 ≤ lift s i j
17   intertwining : ∀ s, (family s).comp V = V.comp (lift s).mulVecLin
18   mass_one : ∀ a x, ∑ o, l (family (a,o) x) = l x
19   initial : E
20   initialCoefficients : J → ℝ
21   initialPrior : FiniteBayes.IsPrior initialCoefficients
22   initial_eq : V initialCoefficients = initial
23 
24 namespace FeasiblePoint
25 variable [DecidableEq J] {V : (J → ℝ) →ₗ[ℝ] E} {l : E →ₗ[ℝ] ℝ}
26 variable (p : FeasiblePoint (A := A) (O := O) V l)
27 
28 theorem valid_family : RobustDomains.ValidFamily (hull V) l p.family :=
29   ⟨fun s => (positive_lift_iff V (p.family s)).mpr
30     ⟨p.lift s,p.nonneg s,p.intertwining s⟩,p.mass_one⟩
31 
32 omit [DecidableEq J] in
33 theorem initial_mem (hn : l.comp V = mass) : p.initial ∈ normalizedHull V l := by
34   rw [← p.initial_eq,normalizedHull_eq_prior_image V l hn]
35   exact ⟨p.initialCoefficients,p.initialPrior,rfl⟩
36 
37 theorem all_word_probabilities (hn : l.comp V = mass) (w : List (A × O)) :
38     0 ≤ l (wordAction p.family w p.initial) ∧ l (wordAction p.family w p.initial) ≤ 1 := by
39   rw [← p.initial_eq]
40   exact (finite_positive_lift_certificate p.family V l hn p.mass_one
41     p.lift p.intertwining p.nonneg p.initialCoefficients p.initialPrior).2.2 w
42 
43 end FeasiblePoint
44 
45 /-- A covered true model with a fixed-domain witness supplies a feasible point. -/
46 theorem feasible_of_certified_member
47     (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
48     (U : Set ((A × O → E →ₗ[ℝ] E) × E))
49     (B : A × O → E →ₗ[ℝ] E) (z : E) (hU : (B,z) ∈ U)
50     (M : A × O → Matrix J J ℝ) (hp : ∀ s i j, 0 ≤ M s i j)
51     (he : ∀ s, (B s).comp V = V.comp (M s).mulVecLin)
52     (hm : ∀ a x, ∑ o, l (B (a,o) x) = l x)
53     (a₀ : J → ℝ) (ha₀ : FiniteBayes.IsPrior a₀) (hz : V a₀ = z) :
54     ∃ p : FeasiblePoint V l, (p.family,p.initial) ∈ U :=
55   ⟨⟨B,M,hp,he,hm,z,a₀,ha₀,hz⟩,hU⟩
56 
57 /-- One normed-space argument applies to both operators and initial states. -/
58 theorem two_center_error {X : Type*} [SeminormedAddCommGroup X]
59     (truth center corrected : X) (ε : ℝ)
60     (ht : ‖truth-center‖ ≤ ε) (hc : ‖corrected-center‖ ≤ ε) :
61     ‖corrected-truth‖ ≤ 2*ε := by
62   calc
63     ‖corrected-truth‖ = ‖(corrected-center)-(truth-center)‖ := by congr 1; abel
64     _ ≤ ‖corrected-center‖ + ‖truth-center‖ := norm_sub_le _ _
65     _ ≤ 2*ε := by linarith
66 
67 end Komorebi.LSM.CertifiedCorrection

Back to source controls