PacketApproximation.lean

1 import KomorebiLSM.Polynomial
2 import KomorebiLSM.DefectPropagation
3 import Mathlib.Analysis.Normed.Module.Multilinear.Basic
4 
5 /-! P20: all ordered packet tuples, an explicit omitted sum and bounded-domain
6 Lipschitz control. No nonlinear independent-packet rule is assumed. -/
7 set_option autoImplicit false
8 open scoped BigOperators
9 namespace Komorebi.LSM.PacketApproximation
10 universe u v w
11 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
12 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
13 variable {Y : Type w} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
14 variable {I : Type*}
15 
16 /-- A bound on B restricted to the specified product of packet ranges. -/
17 def HasPacketBound {m : ℕ} (P : I → X →L[𝕜] X)
18     (B : ContinuousMultilinearMap 𝕜 (fun _ : Fin m => X) Y)
19     (f : Fin m → I) (beta : ℝ) : Prop :=
20   ∀ v : Fin m → X, (∀ k, v k ∈ LinearMap.range (P (f k)).toLinearMap) →
21     ‖B v‖ ≤ beta*∏ k, ‖v k‖
22 
23 theorem projected_packet_bound {m : ℕ} (P : I → X →L[𝕜] X)
24     (B : ContinuousMultilinearMap 𝕜 (fun _ : Fin m => X) Y)
25     (f : Fin m → I) {beta : ℝ} (bound : HasPacketBound P B f beta) (v : Fin m → X) :
26     ‖B (fun k => P (f k) (v k))‖ ≤ beta*∏ k, ‖P (f k) (v k)‖ := by
27   apply bound
28   intro k
29   exact ⟨v k,rfl⟩
30 
31 theorem contractive_packet_norm (P : X →L[𝕜] X) (bound : ‖P‖ ≤ 1) (x : X) :
32     ‖P x‖ ≤ ‖x‖ := by
33   exact (P.le_opNorm x).trans (by simpa using mul_le_mul_of_nonneg_right bound (norm_nonneg x))
34 
35 theorem packet_multilinear_bound {m : ℕ} (P : I → X →L[𝕜] X)
36     (contractive : ∀ i, ‖P i‖ ≤ 1)
37     (B : ContinuousMultilinearMap 𝕜 (fun _ : Fin m => X) Y)
38     (f : Fin m → I) {beta : ℝ} (hbeta : 0 ≤ beta)
39     (bound : HasPacketBound P B f beta) (v : Fin m → X) :
40     ‖B (fun k => P (f k) (v k))‖ ≤ beta*∏ k, ‖v k‖ := by
41   apply (projected_packet_bound P B f bound v).trans
42   apply mul_le_mul_of_nonneg_left _ hbeta
43   exact Finset.prod_le_prod (fun _ _ => norm_nonneg _)
44     (fun k _ => contractive_packet_norm _ (contractive _) (v k))
45 
46 /-- Telescoping multilinearity gives the degree factor. -/
47 theorem packet_term_lipschitz {m : ℕ} (P : I → X →L[𝕜] X)
48     (contractive : ∀ i, ‖P i‖ ≤ 1)
49     (B : ContinuousMultilinearMap 𝕜 (fun _ : Fin (m+1) => X) Y)
50     (f : Fin (m+1) → I) {beta R : ℝ} (hbeta : 0 ≤ beta) (hR : 0 ≤ R)
51     (bound : HasPacketBound P B f beta) (x y : X) (hx : ‖x‖ ≤ R) (hy : ‖y‖ ≤ R) :
52     ‖B (fun k => P (f k) x)-B (fun k => P (f k) y)‖ ≤
53       ((m+1:ℕ):ℝ)*beta*R^m*‖x-y‖ := by
54   let T := B.toMultilinearMap.compLinearMap (fun k => (P (f k)).toLinearMap)
55   have hb : ∀ v, ‖T v‖ ≤ beta*∏ k, ‖v k‖ :=
56     packet_multilinear_bound P contractive B f hbeta bound
57   have h := T.norm_image_sub_le_of_bound hbeta hb (fun _ => x) (fun _ => y)
58   have hmax : max ‖(fun _ : Fin (m+1) => x)‖ ‖(fun _ : Fin (m+1) => y)‖ ≤ R := by
59     exact max_le ((pi_norm_le_iff_of_nonneg hR).mpr (fun _ => hx))
60       ((pi_norm_le_iff_of_nonneg hR).mpr (fun _ => hy))
61   have hdiff : ‖(fun _ : Fin (m+1) => x)-(fun _ : Fin (m+1) => y)‖ ≤ ‖x-y‖ := by
62     exact (pi_norm_le_iff_of_nonneg (norm_nonneg _)).mpr (fun _ => le_rfl)
63   simp only [Fintype.card_fin, Nat.add_sub_cancel] at h
64   calc
65     _ ≤ beta*(m+1:ℕ)*max ‖(fun _ : Fin (m+1) => x)‖ ‖(fun _ : Fin (m+1) => y)‖^m*
66         ‖(fun _ : Fin (m+1) => x)-(fun _ : Fin (m+1) => y)‖ := h
67     _ ≤ beta*(m+1:ℕ)*R^m*‖x-y‖ := by gcongr
68     _ = _ := by ring
69 
70 def fullPolynomial (p : ℕ)
71     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
72     (b : Y) (x : X) : Y := b+∑ m, B m (fun _ => x)
73 
74 variable [Fintype I]
75 
76 def retainedPolynomial (p : ℕ) (P : I → X →L[𝕜] X)
77     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
78     (keep : (m : Fin p) → Finset (Fin (m.val+1) → I)) (b : Y) (x : X) : Y :=
79   b+∑ m, ∑ f ∈ keep m, B m (fun k => P (f k) x)
80 
81 theorem full_ordered_expansion (p : ℕ) (P : I → X →L[𝕜] X)
82     (complete : ∀ x, ∑ i, P i x=x)
83     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
84     (b : Y) (x : X) :
85     fullPolynomial p B b x = b+∑ m, ∑ f : Fin (m.val+1) → I, B m (fun k => P (f k) x) := by
86   unfold fullPolynomial
87   congr 1
88   apply Finset.sum_congr rfl
89   intro m _
90   have h := (B m).toMultilinearMap.map_sum (fun (_ : Fin (m.val+1)) i => P i x)
91   simpa only [complete, ContinuousMultilinearMap.coe_coe] using h
92 
93 /-- The difference is literally the sum of omitted ordered interactions. -/
94 theorem omitted_interaction_identity [DecidableEq I] (p : ℕ) (P : I → X →L[𝕜] X)
95     (complete : ∀ x, ∑ i, P i x=x)
96     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
97     (keep : (m : Fin p) → Finset (Fin (m.val+1) → I)) (b : Y) (x : X) :
98     fullPolynomial p B b x-retainedPolynomial p P B keep b x =
99       ∑ m, ∑ f ∈ Finset.univ \ keep m, B m (fun k => P (f k) x) := by
100   classical
101   rw [full_ordered_expansion p P complete B b x]
102   unfold retainedPolynomial
103   simp only [add_sub_add_left_eq_sub, ← Finset.sum_sub_distrib]
104   apply Finset.sum_congr rfl
105   intro m _
106   exact (Finset.sum_sdiff_eq_sub (Finset.subset_univ (keep m))).symm
107 
108 /-- Restricted block bounds and packet amplitudes yield the stated remainder. -/
109 theorem packet_interaction_truncation_bound [DecidableEq I] (p : ℕ) (P : I → X →L[𝕜] X)
110     (complete : ∀ x, ∑ i, P i x=x)
111     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
112     (keep : (m : Fin p) → Finset (Fin (m.val+1) → I))
113     (beta : (m : Fin p) → (Fin (m.val+1) → I) → ℝ)
114     (bound : ∀ m f, HasPacketBound P (B m) f (beta m f)) (b : Y) (x : X) :
115     ‖fullPolynomial p B b x-retainedPolynomial p P B keep b x‖ ≤
116       ∑ m, ∑ f ∈ Finset.univ \ keep m, beta m f*∏ k, ‖P (f k) x‖ := by
117   classical
118   rw [omitted_interaction_identity p P complete B keep b x]
119   apply (norm_sum_le _ _).trans
120   apply Finset.sum_le_sum
121   intro m _
122   apply (norm_sum_le _ _).trans
123   exact Finset.sum_le_sum (fun f _ => projected_packet_bound P (B m) f (bound m f) (fun _ => x))
124 
125 omit [Fintype I] in
126 /-- A bounded-domain norm inequality equivalent to the displayed Lipschitz bound. -/
127 theorem retained_polynomial_lipschitz_bound (p : ℕ) (P : I → X →L[𝕜] X)
128     (contractive : ∀ i, ‖P i‖ ≤ 1)
129     (B : (m : Fin p) → ContinuousMultilinearMap 𝕜 (fun _ : Fin (m.val+1) => X) Y)
130     (keep : (m : Fin p) → Finset (Fin (m.val+1) → I))
131     (beta : (m : Fin p) → (Fin (m.val+1) → I) → ℝ)
132     (hbeta : ∀ m f, 0 ≤ beta m f)
133     (bound : ∀ m f, HasPacketBound P (B m) f (beta m f))
134     (b : Y) {R : ℝ} (hR : 0 ≤ R) (x y : X) (hx : ‖x‖ ≤ R) (hy : ‖y‖ ≤ R) :
135     ‖retainedPolynomial p P B keep b x-retainedPolynomial p P B keep b y‖ ≤
136       (∑ m, ∑ f ∈ keep m, (m.val+1:ℕ)*beta m f*R^m.val)*‖x-y‖ := by
137   classical
138   unfold retainedPolynomial
139   simp only [add_sub_add_left_eq_sub, ← Finset.sum_sub_distrib]
140   apply (norm_sum_le _ _).trans
141   rw [Finset.sum_mul]
142   apply Finset.sum_le_sum
143   intro m _
144   apply (norm_sum_le _ _).trans
145   rw [Finset.sum_mul]
146   exact Finset.sum_le_sum (fun f _ =>
147     packet_term_lipschitz P contractive (B m) f (hbeta m f) hR (bound m f) x y hx hy)
148 
149 omit [NormedAddCommGroup X] in
150 /-- A physical-model remainder is added explicitly instead of silently equating
151 the polynomial with an unexpanded nonlinear law. -/
152 theorem additional_model_remainder (f poly approx : X → Y) (x : X) {eps tail : ℝ}
153     (model_error : ‖f x-poly x‖ ≤ eps) (truncation : ‖poly x-approx x‖ ≤ tail) :
154     ‖f x-approx x‖ ≤ eps+tail := by
155   calc
156     ‖f x-approx x‖ = ‖(f x-poly x)+(poly x-approx x)‖ := by congr 1; abel
157     _ ≤ ‖f x-poly x‖+‖poly x-approx x‖ := norm_add_le _ _
158     _ ≤ _ := add_le_add model_error truncation
159 
160 end Komorebi.LSM.PacketApproximation

Back to source controls