KrylovPackets.lean

1 module
2 public import LowRankChains
3 import all LowRankChains
4 import all LowRankAlgebra
5 import all ProductChainError
6 import all QuantumPacketCore
7 public import Mathlib.Topology.MetricSpace.HausdorffDistance
8 public import Mathlib.Analysis.Normed.Operator.NormedSpace
9 public import Mathlib.LinearAlgebra.Span.Basic
10 public import Mathlib.Tactic
11 
12 /-!
13 Author: Komorebi P.
14 Paper VIII 7.2 and 7.3. Actual Krylov submodules, independently defined as
15 spans of finite operator orbits. Directness is proved from the packet ranges.
16 The distance certificate is for the actual metric infimum distance.
17 No condition-number or conjugate-gradient convergence theorem is claimed here.
18 -/
19 public section
20 set_option autoImplicit false
21 set_option backward.isDefEq.respectTransparency false
22 set_option backward.isDefEq.respectTransparency.types false
23 namespace KomorebiPaperVIII
24 open scoped BigOperators
25 open KomorebiPaperVII
26 
27 section Algebra
28 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
29 
30 /-- Zero cross-packet transfer implies actual commutation with every projector. -/
31 theorem packet_diagonal_commutes (P : PacketFamily R I) (D : R)
32     (hD : PacketDiagonal P D) (i : I) : Commute D (P.proj i) := by
33   have hc : (∑ b, P.block D b i) = P.block D i i := by
34     apply Finset.sum_eq_single i
35     · intro b _ hbi
36       exact hD b i hbi
37     · simp
38   have hr : (∑ a, P.block D i a) = P.block D i i := by
39     apply Finset.sum_eq_single i
40     · intro a _ hai
41       exact hD i a hai.symm
42     · simp
43   have hcl : (∑ b, P.block D b i) = D * P.proj i := by
44     simp only [PacketFamily.block, ← Finset.sum_mul, P.sum_proj, one_mul]
45   have hrl : (∑ a, P.block D i a) = P.proj i * D := by
46     simp only [PacketFamily.block, ← Finset.mul_sum, P.sum_proj, mul_one]
47   exact hcl.symm.trans (hc.trans (hr.symm.trans hrl))
48 
49 /-- Powers of the local block agree with full powers on that packet's range. -/
50 theorem power_on_packet (P : PacketFamily R I) (A : R)
51     (hA : ∀ i, Commute A (P.proj i)) (i : I) (j : ℕ) :
52     (P.block A i i) ^ j * P.proj i = A ^ j * P.proj i := by
53   have hb : P.block A i i = A * P.proj i := by
54     rw [PacketFamily.block, ← (hA i).eq, mul_assoc, P.idempotent]
55   have hp : ∀ j : ℕ, P.proj i ^ j * P.proj i = P.proj i := by
56     intro k
57     induction k with
58     | zero => simp
59     | succ k ih => simpa only [pow_succ, mul_assoc, P.idempotent] using ih
60   rw [hb, (hA i).mul_pow, mul_assoc, hp]
61 end Algebra
62 
63 section Krylov
64 variable {K X I : Type*} [NontriviallyNormedField K]
65 variable [NormedAddCommGroup X] [NormedSpace K X] [Fintype I] [DecidableEq I]
66 
67 /-- Span of v, A v, ..., A^(m-1) v; m=0 is the zero subspace. -/
68 def krylovSpace (A : X →L[K] X) (v : X) (m : ℕ) : Submodule K X :=
69   Submodule.span K (Set.range (fun j : Fin m => (A ^ j.val) v))
70 
71 theorem krylov_generator_mem (A : X →L[K] X) (v : X) (m j : ℕ) (hj : j < m) :
72     (A ^ j) v ∈ krylovSpace A v m :=
73   Submodule.subset_span ⟨⟨j, hj⟩, rfl⟩
74 
75 /-- Proposition 7.2: exact decomposition of every actual iterate. -/
76 theorem invariant_packet_power_expansion (P : PacketFamily (X →L[K] X) I)
77     (A : X →L[K] X) (hA : ∀ i, Commute A (P.proj i)) (v : X) (j : ℕ) :
78     (A ^ j) v = ∑ i, ((P.block A i i) ^ j) (P.proj i v) := by
79   have hv : ∑ i, P.proj i v = v := by
80     simpa only [sum_apply, one_apply_eq_self] using
81       congrArg (fun (T : X →L[K] X) => T v) P.sum_proj
82   calc
83     (A ^ j) v = (A ^ j) (∑ i, P.proj i v) := by rw [hv]
84     _ = ∑ i, (A ^ j) (P.proj i v) := map_sum _ _ _
85     _ = _ := Finset.sum_congr rfl (fun i _ =>
86       (congrArg (fun (T : X →L[K] X) => T v) (power_on_packet P A hA i j)).symm)
87 
88 /-- Proposition 7.2: inclusion of actual Krylov spans in the sum of the local spans. -/
89 theorem invariant_packet_krylov (P : PacketFamily (X →L[K] X) I)
90     (A : X →L[K] X) (hA : ∀ i, Commute A (P.proj i)) (v : X) (m : ℕ) :
91     krylovSpace A v m ≤ ⨆ i, krylovSpace (P.block A i i) (P.proj i v) m := by
92   apply Submodule.span_le.mpr
93   rintro x ⟨j, rfl⟩
94   change (A ^ j.val) v ∈ (⨆ i, krylovSpace (P.block A i i) (P.proj i v) m : Submodule K X)
95   rw [invariant_packet_power_expansion P A hA v j.val]
96   apply Submodule.sum_mem
97   intro i _
98   exact Submodule.mem_iSup_of_mem i
99     (krylov_generator_mem (P.block A i i) (P.proj i v) m j.val j.isLt)
100 
101 /-- Local Krylov spaces stay in their actual projector ranges. -/
102 theorem local_krylov_le_range (P : PacketFamily (X →L[K] X) I)
103     (A : X →L[K] X) (v : X) (m : ℕ) (i : I) :
104     krylovSpace (P.block A i i) (P.proj i v) m ≤ LinearMap.range (P.proj i).toLinearMap := by
105   apply Submodule.span_le.mpr
106   rintro x ⟨j, rfl⟩
107   cases hj : j.val with
108   | zero => exact ⟨v, by simp [hj]⟩
109   | succ n =>
110     refine ⟨A (P.proj i (((P.block A i i) ^ n) (P.proj i v))), ?_⟩
111     simp only [hj, pow_succ', PacketFamily.block, mul_apply_eq_comp,
112       ContinuousLinearMap.coe_coe]
113 
114 /-- Projecting a finite sum of range-supported vectors selects exactly one term. -/
115 theorem project_packet_sum (P : PacketFamily (X →L[K] X) I) (x : I → X)
116     (hx : ∀ i, x i ∈ LinearMap.range (P.proj i).toLinearMap) (j : I) :
117     P.proj j (∑ i, x i) = x j := by
118   have ht (i : I) : P.proj j (x i) = if j = i then x i else 0 := by
119     obtain ⟨v, hv⟩ := hx i
120     change P.proj i v = x i at hv
121     rw [← hv]
122     have hm := congrArg (fun (T : X →L[K] X) => T v) (P.mul_proj j i)
123     by_cases hji : j = i
124     · subst j
125       simpa only [ite_true, mul_apply_eq_comp] using hm
126     · simpa [hji] using hm
127   simp only [map_sum, ht]
128   simp
129 
130 /-- The sum in Proposition 7.2 is direct: a zero local decomposition is termwise zero. -/
131 theorem local_krylov_direct (P : PacketFamily (X →L[K] X) I)
132     (A : X →L[K] X) (v : X) (m : ℕ) (x : I → X)
133     (hx : ∀ i, x i ∈ krylovSpace (P.block A i i) (P.proj i v) m)
134     (hsum : ∑ i, x i = 0) : ∀ i, x i = 0 := by
135   intro i
136   have h := project_packet_sum P x (fun j => local_krylov_le_range P A v m j (hx j)) i
137   simpa only [hsum, map_zero] using h.symm
138 end Krylov
139 
140 section PowerBound
141 variable {R : Type*} [NormedRing R]
142 
143 /-- A sharp first-order power perturbation bound valid even in the trivial ring. -/
144 theorem power_difference_bound_succ (A D : R) (n : ℕ) :
145     ‖A ^ (n + 1) - D ^ (n + 1)‖ ≤
146       ((n + 1 : ℕ) : ℝ) * (max ‖A‖ ‖D‖) ^ n * ‖A - D‖ := by
147   let M := max ‖A‖ ‖D‖
148   have hM : 0 ≤ M := (norm_nonneg A).trans (le_max_left _ _)
149   have hA : ‖A‖ ≤ M := le_max_left _ _
150   have hD : ‖D‖ ≤ M := le_max_right _ _
151   induction n with
152   | zero => simp
153   | succ n ih =>
154     have hid : A ^ (n + 1 + 1) - D ^ (n + 1 + 1) =
155         A * (A ^ (n + 1) - D ^ (n + 1)) + (A - D) * D ^ (n + 1) := by
156       rw [pow_succ' A (n + 1), pow_succ' D (n + 1)]
157       noncomm_ring
158     have hp : ‖D ^ (n + 1)‖ ≤ M ^ (n + 1) :=
159       (norm_pow_le' D (Nat.succ_pos n)).trans (pow_le_pow_left₀ (norm_nonneg D) hD _)
160     calc
161       _ = ‖A * (A ^ (n + 1) - D ^ (n + 1)) + (A - D) * D ^ (n + 1)‖ := by rw [hid]
162       _ ≤ ‖A‖ * ‖A ^ (n + 1) - D ^ (n + 1)‖ + ‖A - D‖ * ‖D ^ (n + 1)‖ :=
163         (norm_add_le _ _).trans (add_le_add (norm_mul_le _ _) (norm_mul_le _ _))
164       _ ≤ M * (((n + 1 : ℕ) : ℝ) * M ^ n * ‖A - D‖) + ‖A - D‖ * M ^ (n + 1) :=
165         add_le_add (mul_le_mul hA ih (norm_nonneg _) hM)
166           (mul_le_mul_of_nonneg_left hp (norm_nonneg _))
167       _ = _ := by dsimp [M]; push_cast; rw [pow_succ]; ring
168 
169 /-- Theorem 7.3's operator estimate in the manuscript's positive-index convention. -/
170 theorem approximate_packet_power_bound (D K : R) (j : ℕ) (hj : 0 < j) :
171     ‖(D + K) ^ j - D ^ j‖ ≤
172       (j : ℝ) * (max ‖D + K‖ ‖D‖) ^ (j - 1) * ‖K‖ := by
173   have h := power_difference_bound_succ (D + K) D (j - 1)
174   have he : j - 1 + 1 = j := by omega
175   simpa only [he, add_sub_cancel_left] using h
176 end PowerBound
177 
178 section Distance
179 variable {K X I : Type*} [NontriviallyNormedField K]
180 variable [NormedAddCommGroup X] [NormedSpace K X] [Fintype I] [DecidableEq I]
181 
182 /-- Theorem 7.3's actual distance-to-local-Krylov-space certificate. -/
183 theorem approximate_packet_krylov_distance (P : PacketFamily (X →L[K] X) I)
184     (D E : X →L[K] X) (hD : PacketDiagonal P D) (v : X) (j : ℕ) (hj : 0 < j) :
185     Metric.infDist (((D + E) ^ j) v)
186       ((⨆ i, krylovSpace (P.block D i i) (P.proj i v) (j + 1) : Submodule K X) : Set X) ≤
187       (j : ℝ) * (max ‖D + E‖ ‖D‖) ^ (j - 1) * ‖E‖ * ‖v‖ := by
188   have hm : (D ^ j) v ∈ (⨆ i, krylovSpace (P.block D i i) (P.proj i v) (j + 1) : Submodule K X) :=
189     invariant_packet_krylov P D (packet_diagonal_commutes P D hD) v (j + 1)
190       (krylov_generator_mem D v (j + 1) j (Nat.lt_succ_self j))
191   calc
192     _ ≤ dist (((D + E) ^ j) v) ((D ^ j) v) := Metric.infDist_le_dist_of_mem hm
193     _ = ‖((D + E) ^ j - D ^ j) v‖ := by rw [dist_eq_norm]; rfl
194     _ ≤ ‖(D + E) ^ j - D ^ j‖ * ‖v‖ := ((D + E) ^ j - D ^ j).le_opNorm v
195     _ ≤ _ := mul_le_mul_of_nonneg_right (approximate_packet_power_bound D E j hj) (norm_nonneg _)
196 end Distance
197 end KomorebiPaperVIII
198 
199 #print axioms KomorebiPaperVIII.packet_diagonal_commutes
200 #print axioms KomorebiPaperVIII.power_on_packet
201 #print axioms KomorebiPaperVIII.krylov_generator_mem
202 #print axioms KomorebiPaperVIII.invariant_packet_power_expansion
203 #print axioms KomorebiPaperVIII.invariant_packet_krylov
204 #print axioms KomorebiPaperVIII.local_krylov_le_range
205 #print axioms KomorebiPaperVIII.project_packet_sum
206 #print axioms KomorebiPaperVIII.local_krylov_direct
207 #print axioms KomorebiPaperVIII.power_difference_bound_succ
208 #print axioms KomorebiPaperVIII.approximate_packet_power_bound
209 #print axioms KomorebiPaperVIII.approximate_packet_krylov_distance

Back to source controls