ProductChainError.lean

1 module
2 public import PacketPerturbation
3 import all PacketPerturbation
4 public import Mathlib.Analysis.Normed.Operator.NormedSpace
5 public import Mathlib.Analysis.Normed.Ring.Basic
6 public import Mathlib.Algebra.BigOperators.Intervals
7 public import Mathlib.Tactic
8 
9 /-!
10 Author: Komorebi P.
11 Paper VIII 5.8, 5.9 and 8.3. Actual noncommutative products and actual
12 recompressed iterates, with closed finite-sum error certificates.
13 Indices are zero based: factor j in Lean is manuscript factor j+1.
14 No commutativity of operators or implementation rounding model is assumed.
15 -/
16 public section
17 set_option autoImplicit false
18 namespace KomorebiPaperVIII
19 open scoped BigOperators
20 
21 /-- The left-accumulated product A(n-1) ... A(0). -/
22 def chainProduct {R : Type*} [Monoid R] (A : ℕ → R) : ℕ → R
23   | 0 => 1
24   | n + 1 => A n * chainProduct A n
25 
26 /-- An actual iteration that introduces additive error after each product. -/
27 def recompressedProduct {R : Type*} [Ring R] (A E : ℕ → R) : ℕ → R
28   | 0 => 1
29   | n + 1 => A n * recompressedProduct A E n + E n
30 
31 /-- Scalar propagation, independent of the operator iterates. -/
32 def propagatedError (a e : ℕ → ℝ) : ℕ → ℝ
33   | 0 => 0
34   | n + 1 => a n * propagatedError a e n + e n
35 
36 /-- Closed form, with empty suffix products equal to one. -/
37 theorem propagatedError_eq_sum (a e : ℕ → ℝ) (n : ℕ) :
38     propagatedError a e n =
39       ∑ j ∈ Finset.range n, (∏ i ∈ Finset.Ico (j + 1) n, a i) * e j := by
40   induction n with
41   | zero => simp [propagatedError]
42   | succ n ih =>
43     rw [propagatedError, ih, Finset.sum_range_succ, Finset.mul_sum]
44     congr 1
45     · apply Finset.sum_congr rfl
46       intro j hj
47       have hjn : j + 1 ≤ n := Finset.mem_range.mp hj
48       rw [Finset.prod_Ico_succ_top hjn]
49       ring
50     · simp
51 
52 /-- Monotonicity in certified local error budgets. -/
53 theorem propagatedError_mono (a e d : ℕ → ℝ) (ha : ∀ n, 0 ≤ a n)
54     (hed : ∀ n, e n ≤ d n) (n : ℕ) :
55     propagatedError a e n ≤ propagatedError a d n := by
56   induction n with
57   | zero => exact le_rfl
58   | succ n ih =>
59     exact add_le_add (mul_le_mul_of_nonneg_left ih (ha n)) (hed n)
60 
61 /-- A nonnegative gain recurrence dominates actual norm errors. -/
62 theorem norm_recurrence_bound {R : Type*} [SeminormedAddCommGroup R]
63     (D : ℕ → R) (a e : ℕ → ℝ) (hzero : D 0 = 0) (ha : ∀ n, 0 ≤ a n)
64     (hstep : ∀ n, ‖D (n + 1)‖ ≤ a n * ‖D n‖ + e n) (n : ℕ) :
65     ‖D n‖ ≤ propagatedError a e n := by
66   induction n with
67   | zero => simp [hzero, propagatedError]
68   | succ n ih =>
69     exact (hstep n).trans (add_le_add (mul_le_mul_of_nonneg_left ih (ha n)) le_rfl)
70 
71 section Ring
72 variable {R : Type*} [Ring R]
73 
74 /-- The discrepancy recursion is derived from multiplication, not assumed. -/
75 theorem product_discrepancy_step (A B : ℕ → R) (n : ℕ) :
76     chainProduct B (n + 1) - chainProduct A (n + 1) =
77       B n * (chainProduct B n - chainProduct A n) +
78       (B n - A n) * chainProduct A n := by
79   simp only [chainProduct]
80   noncomm_ring
81 
82 /-- The corresponding exact identity for additive post-product recompression. -/
83 theorem recompression_discrepancy_step (A E : ℕ → R) (n : ℕ) :
84     recompressedProduct A E (n + 1) - chainProduct A (n + 1) =
85       A n * (recompressedProduct A E n - chainProduct A n) + E n := by
86   simp only [recompressedProduct, chainProduct]
87   noncomm_ring
88 
89 /-- Constant-factor products are the actual ring power. -/
90 theorem chainProduct_const (A : R) (n : ℕ) : chainProduct (fun _ => A) n = A ^ n := by
91   induction n with
92   | zero => simp [chainProduct]
93   | succ n ih => simp [chainProduct, ih, pow_succ']
94 end Ring
95 
96 section NormedRing
97 variable {R : Type*} [NormedRing R]
98 
99 /-- Theorem 5.9, including a user-supplied bound on every recompression residual. -/
100 theorem repeated_recompression_bound (A E : ℕ → R) (δ : ℕ → ℝ)
101     (hδ : ∀ j, ‖E j‖ ≤ δ j) (n : ℕ) :
102     ‖recompressedProduct A E n - chainProduct A n‖ ≤
103       ∑ j ∈ Finset.range n, (∏ i ∈ Finset.Ico (j + 1) n, ‖A i‖) * δ j := by
104   rw [← propagatedError_eq_sum]
105   apply norm_recurrence_bound
106       (fun k => recompressedProduct A E k - chainProduct A k)
107       (fun k => ‖A k‖) δ (by simp [chainProduct, recompressedProduct])
108       (fun k => norm_nonneg _)
109   intro k
110   rw [recompression_discrepancy_step]
111   exact (norm_add_le _ _).trans (add_le_add (norm_mul_le _ _) (hδ k))
112 
113 /-- Theorem 5.9 with the actual residual norms, with no uniform-tolerance assumption. -/
114 theorem repeated_recompression_actual_error (A E : ℕ → R) (n : ℕ) :
115     ‖recompressedProduct A E n - chainProduct A n‖ ≤
116       ∑ j ∈ Finset.range n, (∏ i ∈ Finset.Ico (j + 1) n, ‖A i‖) * ‖E j‖ :=
117   repeated_recompression_bound A E (fun j => ‖E j‖) (fun _ => le_rfl) n
118 
119 /-- Exact products have the expected product-of-norms bound. -/
120 theorem chainProduct_norm_bound [NormOneClass R] (A : ℕ → R) (n : ℕ) :
121     ‖chainProduct A n‖ ≤ ∏ j ∈ Finset.range n, ‖A j‖ := by
122   induction n with
123   | zero => simp [chainProduct]
124   | succ n ih =>
125     rw [chainProduct, Finset.prod_range_succ]
126     exact (norm_mul_le _ _).trans (by nlinarith [norm_nonneg (A n)])
127 
128 /-- Theorem 5.8, with arbitrary certified per-factor operator errors. -/
129 theorem product_chain_error_bound [NormOneClass R] (A B : ℕ → R) (δ : ℕ → ℝ)
130     (hδ : ∀ j, ‖B j - A j‖ ≤ δ j) (n : ℕ) :
131     ‖chainProduct B n - chainProduct A n‖ ≤
132       ∑ j ∈ Finset.range n,
133         (∏ i ∈ Finset.Ico (j + 1) n, ‖B i‖) *
134           (δ j * ∏ i ∈ Finset.range j, ‖A i‖) := by
135   rw [← propagatedError_eq_sum]
136   apply norm_recurrence_bound (fun k => chainProduct B k - chainProduct A k)
137     (fun k => ‖B k‖) (fun k => δ k * ∏ i ∈ Finset.range k, ‖A i‖)
138     (by simp [chainProduct]) (fun k => norm_nonneg _)
139   intro k
140   rw [product_discrepancy_step]
141   apply (norm_add_le _ _).trans
142   apply add_le_add (norm_mul_le _ _)
143   apply (norm_mul_le _ _).trans
144   exact mul_le_mul (hδ k) (chainProduct_norm_bound A k) (norm_nonneg _)
145     ((norm_nonneg _).trans (hδ k))
146 
147 /-- The displayed product-chain bound, for actual additive perturbations. -/
148 theorem product_chain_perturbation [NormOneClass R] (A E : ℕ → R) (n : ℕ) :
149     ‖chainProduct (fun j => A j + E j) n - chainProduct A n‖ ≤
150       ∑ j ∈ Finset.range n,
151         (∏ i ∈ Finset.Ico (j + 1) n, ‖A i + E i‖) *
152           ‖E j‖ * (∏ i ∈ Finset.range j, ‖A i‖) := by
153   simpa only [add_sub_cancel_left, mul_assoc] using
154     product_chain_error_bound A (fun j => A j + E j) (fun j => ‖E j‖)
155       (fun j => by simp) n
156 end NormedRing
157 
158 section PacketChains
159 variable {K X I E : Type*} [NontriviallyNormedField K]
160 variable [NormedAddCommGroup X] [NormedSpace K X] [Nontrivial X] [Fintype E]
161 
162 /-- Corollary 8.3, with the preceding packet certificate substituted stage by stage.
163 This is an operator-norm certificate, not a vector-specific error used as one. -/
164 theorem mixed_precision_product_chain
165     (P : ℕ → I → X →L[K] X) (src : ℕ → E → I)
166     (A Δ : ℕ → E → X →L[K] X)
167     (hΔ : ∀ j e, Δ j e = (Δ j e).comp (P j (src j e))) (n : ℕ) :
168     ‖chainProduct (fun j => ∑ e, (A j e + Δ j e)) n -
169       chainProduct (fun j => ∑ e, A j e) n‖ ≤
170       ∑ j ∈ Finset.range n,
171         (∏ i ∈ Finset.Ico (j + 1) n, ‖∑ e, (A i e + Δ i e)‖) *
172           ((∑ e, ‖Δ j e‖ * ‖P j (src j e)‖) *
173             (∏ i ∈ Finset.range j, ‖∑ e, A i e‖)) := by
174   exact product_chain_error_bound (R := X →L[K] X)
175     (fun j => ∑ e, A j e) (fun j => ∑ e, (A j e + Δ j e))
176     (fun j => ∑ e, ‖Δ j e‖ * ‖P j (src j e)‖)
177     (fun j => packet_operator_perturbation_bound (P j) (src j) (A j) (Δ j) (hΔ j)) n
178 
179 /-- The final vector error follows from the verified operator bound. -/
180 theorem chain_action_error {K X : Type*} [NontriviallyNormedField K]
181     [NormedAddCommGroup X] [NormedSpace K X]
182     (A B : ℕ → X →L[K] X) (n : ℕ) (C : ℝ)
183     (h : ‖chainProduct B n - chainProduct A n‖ ≤ C) (x : X) :
184     ‖chainProduct B n x - chainProduct A n x‖ ≤ C * ‖x‖ := by
185   exact ((chainProduct B n - chainProduct A n).le_opNorm x).trans
186     (mul_le_mul_of_nonneg_right h (norm_nonneg x))
187 end PacketChains
188 end KomorebiPaperVIII
189 
190 #print axioms KomorebiPaperVIII.propagatedError_eq_sum
191 #print axioms KomorebiPaperVIII.propagatedError_mono
192 #print axioms KomorebiPaperVIII.norm_recurrence_bound
193 #print axioms KomorebiPaperVIII.product_discrepancy_step
194 #print axioms KomorebiPaperVIII.recompression_discrepancy_step
195 #print axioms KomorebiPaperVIII.chainProduct_const
196 #print axioms KomorebiPaperVIII.repeated_recompression_bound
197 #print axioms KomorebiPaperVIII.repeated_recompression_actual_error
198 #print axioms KomorebiPaperVIII.chainProduct_norm_bound
199 #print axioms KomorebiPaperVIII.product_chain_error_bound
200 #print axioms KomorebiPaperVIII.product_chain_perturbation
201 #print axioms KomorebiPaperVIII.mixed_precision_product_chain
202 #print axioms KomorebiPaperVIII.chain_action_error

Back to source controls