LowRankChains.lean

1 module
2 public import LowRankAlgebra
3 import all LowRankAlgebra
4 import all PacketIR
5 import all QuantumPacketCore
6 public import ProductChainError
7 import all ProductChainError
8 
9 /-!
10 Author: Komorebi P.
11 Paper VIII 5.2: explicit factor construction for arbitrary product length,
12 variable per-factor ranks, including rank zero and the empty product.
13 The correction-rank bound is actual matrix rank, not only a storage count.
14 -/
15 public section
16 set_option autoImplicit false
17 set_option backward.isDefEq.respectTransparency false
18 set_option backward.isDefEq.respectTransparency.types false
19 namespace KomorebiPaperVIII
20 open scoped BigOperators
21 open KomorebiPaperVII
22 
23 /-- Columns are concatenated at every multiplication, without recompression. -/
24 @[expose] def ChainColumns (r : ℕ → ℕ) : ℕ → Type
25   | 0 => Fin 0
26   | n + 1 => ChainColumns r n ⊕ Fin (r n)
27 
28 instance chainColumnsFintype (r : ℕ → ℕ) : (n : ℕ) → Fintype (ChainColumns r n)
29   | 0 => inferInstanceAs (Fintype (Fin 0))
30   | n + 1 =>
31     letI := chainColumnsFintype r n
32     inferInstanceAs (Fintype (ChainColumns r n ⊕ Fin (r n)))
33 
34 theorem chainColumns_card (r : ℕ → ℕ) (n : ℕ) :
35     Fintype.card (ChainColumns r n) = ∑ j ∈ Finset.range n, r j := by
36   induction n with
37   | zero => simp [ChainColumns]
38   | succ n ih =>
39     change Fintype.card (ChainColumns r n ⊕ Fin (r n)) = _
40     simp only [Fintype.card_sum, Fintype.card_fin, ih, Finset.sum_range_succ]
41 
42 section FactorConstruction
43 variable {K X : Type*} [Field K] [StarRing K] [Fintype X] [DecidableEq X]
44 variable (r : ℕ → ℕ) (D : ℕ → Matrix X X K)
45 variable (U V : (j : ℕ) → Matrix X (Fin (r j)) K)
46 
47 /-- The actual pair of thin factors is recursively constructed using the checked two-factor rule. -/
48 def chainFactors : (n : ℕ) → Matrix X (ChainColumns r n) K × Matrix X (ChainColumns r n) K
49   | 0 => (0, 0)
50   | n + 1 =>
51     let prior := chainFactors n
52     (bdlrProductLeft (D n) (U n) (V n) prior.1,
53       bdlrProductRight (chainProduct D n) (V n) prior.2)
54 
55 /-- The constructed factors represent the exact product, not a low-rank approximation. -/
56 theorem chainFactors_correct (n : ℕ) :
57     chainProduct (fun j => D j + U j * (V j).conjTranspose) n =
58       chainProduct D n + (chainFactors r D U V n).1 * (chainFactors r D U V n).2.conjTranspose := by
59   induction n with
60   | zero =>
61     ext i j
62     simp [chainProduct, chainFactors, ChainColumns]
63   | succ n ih =>
64     rw [chainProduct, ih]
65     exact bdlr_product (D n) (chainProduct D n) (U n) (V n)
66       (chainFactors r D U V n).1 (chainFactors r D U V n).2
67 
68 /-- Corollary 5.2: actual matrix rank of the complete correction is bounded additively. -/
69 theorem bdlr_chain_rank_bound (n : ℕ) :
70     (chainProduct (fun j => D j + U j * (V j).conjTranspose) n - chainProduct D n).rank ≤
71       ∑ j ∈ Finset.range n, r j := by
72   rw [chainFactors_correct, add_sub_cancel_left]
73   calc
74     _ ≤ (chainFactors r D U V n).1.rank := Matrix.rank_mul_le_left _ _
75     _ ≤ Fintype.card (ChainColumns r n) := Matrix.rank_le_card_width _
76     _ = _ := chainColumns_card r n
77 end FactorConstruction
78 
79 section Diagonal
80 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
81 
82 theorem packet_diagonal_one (P : PacketFamily R I) : PacketDiagonal P (1 : R) := by
83   intro b a hba
84   simp [PacketFamily.block, P.mul_proj, hba]
85 
86 /-- The base part stays packet diagonal at every length, including the identity. -/
87 theorem packet_diagonal_chain (P : PacketFamily R I) (D : ℕ → R)
88     (hD : ∀ j, PacketDiagonal P (D j)) (n : ℕ) : PacketDiagonal P (chainProduct D n) := by
89   induction n with
90   | zero => exact packet_diagonal_one P
91   | succ n ih => exact packet_diagonal_product P (D n) (chainProduct D n) (hD n) ih
92 end Diagonal
93 end KomorebiPaperVIII
94 
95 #print axioms KomorebiPaperVIII.chainColumns_card
96 #print axioms KomorebiPaperVIII.chainFactors_correct
97 #print axioms KomorebiPaperVIII.bdlr_chain_rank_bound
98 #print axioms KomorebiPaperVIII.packet_diagonal_one
99 #print axioms KomorebiPaperVIII.packet_diagonal_chain
100 #print axioms KomorebiPaperVIII.chainFactors

Back to source controls