CompactTruncation.lean

1 module
2 public import DiagonalTruncation
3 import all SmallCoreNorms
4 import all DiagonalTruncation
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Thin square-root factors with exactly min(d,k) columns.
7 Zero singular values never require division. -/
8 public section
9 set_option autoImplicit false
10 namespace KomorebiPaperVIII.SmallCore
11 open scoped BigOperators Matrix Classical
12 variable {m n : Type*} [Fintype m] [Fintype n] {d : ℕ}
13 
14 abbrev KeptColumn (d k : ℕ) := {i : Fin d // i.val < k}
15 
16 theorem keptColumn_card (k : ℕ) : Fintype.card (KeptColumn d k) = min d k := by
17   simpa only [KeptColumn, Fintype.card_subtype] using (Fin.card_filter_val_lt (n := d) (m := k))
18 
19 noncomputable def rootMask (σ : Fin d → ℝ) (k : ℕ) :
20     Matrix (Fin d) (KeptColumn d k) ℂ :=
21   (rootKept σ k).submatrix id Subtype.val
22 
23 theorem rootKept_tail_zero (σ : Fin d → ℝ) (k : ℕ) (i j : Fin d)
24     (hj : ¬ j.val < k) : rootKept σ k i j = 0 := by
25   by_cases h : i = j
26   · subst i
27     simp [rootKept,diag,kept,hj]
28   · simp [rootKept,diag,Matrix.diagonal,h]
29 
30 omit [Fintype m] [Fintype n] in
31 theorem drop_zero_columns (A : Matrix m (Fin d) ℂ) (B : Matrix n (Fin d) ℂ)
32     (k : ℕ) (hA : ∀ i j, ¬ j.val < k → A i j = 0) :
33     (A.submatrix id (Subtype.val : KeptColumn d k → Fin d)) *
34       (B.submatrix id (Subtype.val : KeptColumn d k → Fin d))ᴴ = A*Bᴴ := by
35   ext i j
36   simp only [Matrix.mul_apply,Matrix.conjTranspose_apply,Matrix.submatrix_apply,id_eq]
37   apply Fintype.sum_of_injective (Subtype.val : KeptColumn d k → Fin d) Subtype.val_injective
38   · intro l hl
39     have hnot : ¬ l.val < k := by
40       intro h
41       exact hl ⟨⟨l,h⟩,rfl⟩
42     rw [hA i l hnot,zero_mul]
43   · intro l
44     rfl
45 
46 theorem rootMask_square (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i) (k : ℕ) :
47     rootMask σ k * (rootMask σ k)ᴴ = diag (kept σ k) := by
48   unfold rootMask
49   rw [drop_zero_columns _ _ k (rootKept_tail_zero σ k),rootKept_selfAdjoint,
50     rootKept_square σ hσ]
51 
52 omit [Fintype m] [Fintype n] in
53 theorem thin_factor_product (U : Matrix m (Fin d) ℂ) (V : Matrix n (Fin d) ℂ)
54     (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i) (k : ℕ) :
55     (U*rootMask σ k)*(V*rootMask σ k)ᴴ = lift U V (diag (kept σ k)) := by
56   simp only [Matrix.conjTranspose_mul,Matrix.mul_assoc,lift]
57   rw [←Matrix.mul_assoc (rootMask σ k) (rootMask σ k)ᴴ Vᴴ,rootMask_square σ hσ]
58 
59 end KomorebiPaperVIII.SmallCore
60 
61 -- SIXTH AXIOM AUDITS
62 #print axioms KomorebiPaperVIII.SmallCore.keptColumn_card
63 #print axioms KomorebiPaperVIII.SmallCore.rootKept_tail_zero
64 #print axioms KomorebiPaperVIII.SmallCore.drop_zero_columns
65 #print axioms KomorebiPaperVIII.SmallCore.rootMask_square
66 #print axioms KomorebiPaperVIII.SmallCore.thin_factor_product
67 #print axioms KomorebiPaperVIII.SmallCore.KeptColumn
68 #print axioms KomorebiPaperVIII.SmallCore.rootMask

Back to source controls