DataSelectedGeometry.lean

1 import KomorebiLSM.EuclideanMatrixNorms
2 import KomorebiLSM.RobustOrientedMargin
3 
4 /-! P78: an already justified coverage event survives arbitrary data-dependent
5 geometry selection, and whole-state Euclidean errors pay the actual condition number. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.DataSelectedGeometry
8 open MeasureTheory EuclideanMatrixNorms
9 open scoped Matrix BigOperators ENNReal
10 
11 section Coverage
12 variable {E S G Ω : Type*} [AddCommGroup E] [Module ℝ E]
13 
14 /-- Operators and initial state stay in one fixed predictive coordinate system. -/
15 structure Model (S E : Type*) [AddCommGroup E] [Module ℝ E] where
16   initial : E
17   operator : S → E →ₗ[ℝ] E
18 
19 def DomainValid (domain : G → Set E) (g : G) (M : Model S E) : Prop :=
20   M.initial∈domain g ∧ ∀ s z,z∈domain g → M.operator s z∈domain g
21 
22 /-- The same entire uncertainty set is quantified after geometry selection. -/
23 theorem selected_geometry_on_coverage (domain : G → Set E)
24     (U : Ω → Set (Model S E)) (selected : Ω → G) (truth : Model S E)
25     (verifies : ∀ ω M,M∈U ω → DomainValid domain (selected ω) M) :
26     {ω | truth∈U ω}⊆{ω | DomainValid domain (selected ω) truth} := by
27   intro ω hω
28   exact verifies ω truth hω
29 
30 /-- No union over the possibly infinite collection of geometry proposals is used. -/
31 theorem selected_geometry_probability [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
32     (domain : G → Set E) (U : Ω → Set (Model S E)) (selected : Ω → G) (truth : Model S E)
33     (_hcoverage : MeasurableSet {ω | truth∈U ω})
34     (_hverified : MeasurableSet {ω | DomainValid domain (selected ω) truth})
35     (delta : ℝ≥0∞) (hprob : 1-delta≤μ {ω | truth∈U ω})
36     (verifies : ∀ ω M,M∈U ω → DomainValid domain (selected ω) M) :
37     1-delta≤μ {ω | DomainValid domain (selected ω) truth} :=
38   hprob.trans (measure_mono (selected_geometry_on_coverage domain U selected truth verifies))
39 
40 /-- If a procedure sometimes withholds a result, false acceptance is still
41 contained in the original coverage failure event. -/
42 theorem false_acceptance_subset (domain : G → Set E)
43     (U : Ω → Set (Model S E)) (selected : Ω → G) (truth : Model S E) (accepts : Ω → Prop)
44     (verifies : ∀ ω,accepts ω → ∀ M,M∈U ω → DomainValid domain (selected ω) M) :
45     {ω | accepts ω ∧ ¬DomainValid domain (selected ω) truth}⊆{ω | truth∉U ω} := by
46   intro ω hω hmem
47   exact hω.2 (verifies ω hω.1 truth hmem)
48 
49 theorem false_acceptance_probability [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
50     (domain : G → Set E) (U : Ω → Set (Model S E)) (selected : Ω → G) (truth : Model S E)
51     (accepts : Ω → Prop) (delta : ℝ≥0∞)
52     (_hcoverage : MeasurableSet {ω | truth∉U ω})
53     (_hfailure : MeasurableSet {ω | accepts ω ∧ ¬DomainValid domain (selected ω) truth})
54     (hprob : μ {ω | truth∉U ω}≤delta)
55     (verifies : ∀ ω,accepts ω → ∀ M,M∈U ω → DomainValid domain (selected ω) M) :
56     μ {ω | accepts ω ∧ ¬DomainValid domain (selected ω) truth}≤delta :=
57   (measure_mono (false_acceptance_subset domain U selected truth accepts verifies)).trans hprob
58 end Coverage
59 
60 section EuclideanError
61 variable {D : Type*} [Fintype D] [DecidableEq D]
62 abbrev WholeState (D : Type*) := EuclideanSpace ℝ (Unit ⊕ D)
63 
64 def massPart (y : WholeState D) : ℝ := y (Sum.inl ())
65 noncomputable def spatialPart (y : WholeState D) : EuclideanSpace ℝ D :=
66   WithLp.toLp 2 (fun i => y (Sum.inr i))
67 
68 omit [DecidableEq D] in
69 /-- The whole-state norm here is the Euclidean two-norm, not the Lorentz base norm. -/
70 theorem whole_norm_sq (y : WholeState D) : ‖y‖^2=|massPart y|^2+‖spatialPart y‖^2 := by
71   rw [EuclideanSpace.real_norm_sq_eq,EuclideanSpace.real_norm_sq_eq]
72   simp [massPart,spatialPart,Fintype.sum_sum_type]
73 
74 noncomputable def wholeInput (v : EuclideanSpace ℝ D) : WholeState D :=
75   WithLp.toLp 2 (Sum.elim (fun _ : Unit => (1 : ℝ)) (fun i => v i))
76 
77 omit [Fintype D] [DecidableEq D] in
78 @[simp] theorem wholeInput_mass (v : EuclideanSpace ℝ D) : massPart (wholeInput v)=1 := rfl
79 omit [Fintype D] [DecidableEq D] in
80 @[simp] theorem wholeInput_spatial (v : EuclideanSpace ℝ D) : spatialPart (wholeInput v)=v := by
81   ext i
82   rfl
83 
84 omit [DecidableEq D] in
85 theorem wholeInput_norm_le_sqrt_two (v : EuclideanSpace ℝ D) (hv : ‖v‖≤1) :
86     ‖wholeInput v‖≤Real.sqrt 2 := by
87   have hs := whole_norm_sq (wholeInput v)
88   rw [wholeInput_mass,wholeInput_spatial] at hs
89   norm_num at hs
90   have hroot : (Real.sqrt 2)^2=2 := Real.sq_sqrt (by norm_num)
91   nlinarith [norm_nonneg v,norm_nonneg (wholeInput v),Real.sqrt_nonneg 2]
92 
93 omit [DecidableEq D] in
94 /-- The mass/spatial split costs a second sqrt(2) in the genuine Euclidean norm. -/
95 theorem combined_output_le_sqrt_two (y : WholeState D) :
96     |massPart y|+‖spatialPart y‖≤Real.sqrt 2*‖y‖ := by
97   have hs := whole_norm_sq y
98   have hroot : (Real.sqrt 2)^2=2 := Real.sq_sqrt (by norm_num)
99   have hsq : (|massPart y|+‖spatialPart y‖)^2≤(Real.sqrt 2*‖y‖)^2 := by
100     rw [mul_pow,hroot]
101     nlinarith [sq_nonneg (|massPart y|-‖spatialPart y‖)]
102   exact (sq_le_sq₀ (add_nonneg (abs_nonneg _) (norm_nonneg _))
103     (mul_nonneg (Real.sqrt_nonneg _) (norm_nonneg _))).mp hsq
104 
105 /-- Literal matrix conjugation is the composition of the three Euclidean actions. -/
106 theorem conjugate_action (T Delta : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) (z : WholeState D) :
107     Matrix.toEuclideanCLM (𝕜 := ℝ) (T*Delta*T⁻¹) z=
108       Matrix.toEuclideanCLM (𝕜 := ℝ) T (Matrix.toEuclideanCLM (𝕜 := ℝ) Delta (Matrix.toEuclideanCLM (𝕜 := ℝ) T⁻¹ z)) := by
109   simp only [map_mul]
110   rfl
111 
112 /-- The actual factor two and condition number come from the two Euclidean norm comparisons. -/
113 theorem transformed_combined_error (T Delta : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
114     (e : ℝ) (herror : spectralNorm Delta≤e) (v : EuclideanSpace ℝ D) (hv : ‖v‖≤1) :
115     let y := Matrix.toEuclideanCLM (𝕜 := ℝ) (T*Delta*T⁻¹) (wholeInput v)
116     |massPart y|+‖spatialPart y‖≤2*spectralNorm T*spectralNorm T⁻¹*e := by
117   have he0 : 0≤e := (spectralNorm_nonneg Delta).trans herror
118   have ht0 := spectralNorm_nonneg T
119   have hi0 := spectralNorm_nonneg T⁻¹
120   let z := wholeInput v
121   let Iop := Matrix.toEuclideanCLM (𝕜 := ℝ) T⁻¹
122   let Dop := Matrix.toEuclideanCLM (𝕜 := ℝ) Delta
123   let Top := Matrix.toEuclideanCLM (𝕜 := ℝ) T
124   have hi : ‖Iop z‖≤spectralNorm T⁻¹*Real.sqrt 2 :=
125     (Iop.le_opNorm z).trans (mul_le_mul_of_nonneg_left (wholeInput_norm_le_sqrt_two v hv) hi0)
126   have hd : ‖Dop (Iop z)‖≤e*(spectralNorm T⁻¹*Real.sqrt 2) :=
127     (Dop.le_opNorm (Iop z)).trans
128       ((mul_le_mul_of_nonneg_right herror (norm_nonneg (Iop z))).trans
129         (mul_le_mul_of_nonneg_left hi he0))
130   have ht : ‖Top (Dop (Iop z))‖≤spectralNorm T*e*(spectralNorm T⁻¹*Real.sqrt 2) := by
131     have hp : ‖Top (Dop (Iop z))‖≤spectralNorm T*‖Dop (Iop z)‖ := Top.le_opNorm _
132     exact hp.trans (by simpa only [mul_assoc] using mul_le_mul_of_nonneg_left hd ht0)
133   dsimp only
134   rw [conjugate_action]
135   calc
136     _≤Real.sqrt 2*‖Top (Dop (Iop z))‖ := combined_output_le_sqrt_two _
137     _≤Real.sqrt 2*(spectralNorm T*e*(spectralNorm T⁻¹*Real.sqrt 2)) :=
138       mul_le_mul_of_nonneg_left ht (Real.sqrt_nonneg 2)
139     _=(Real.sqrt 2)^2*(spectralNorm T*spectralNorm T⁻¹*e) := by ring
140     _=2*spectralNorm T*spectralNorm T⁻¹*e := by
141       rw [Real.sq_sqrt (by norm_num : (0 : ℝ)≤2)]
142       ring
143 
144 /-- The same pointwise bound applies to transforms selected after seeing arbitrary data. -/
145 theorem data_selected_transformed_error {Ω : Type*}
146     (T Delta : Ω → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) (e : Ω → ℝ)
147     (herror : ∀ ω,spectralNorm (Delta ω)≤e ω) (ω : Ω)
148     (v : EuclideanSpace ℝ D) (hv : ‖v‖≤1) :
149     let y := Matrix.toEuclideanCLM (𝕜 := ℝ) (T ω*Delta ω*(T ω)⁻¹) (wholeInput v)
150     |massPart y|+‖spatialPart y‖≤2*spectralNorm (T ω)*spectralNorm (T ω)⁻¹*e ω :=
151   transformed_combined_error (T ω) (Delta ω) (e ω) (herror ω) v hv
152 end EuclideanError
153 
154 end Komorebi.LSM.DataSelectedGeometry

Back to source controls