DiagonalTruncation.lean

1 module
2 public import SmallCoreTransfer
3 import all SmallCoreNorms
4 import all SmallCoreTransfer
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Truncated nonnegative diagonal data, exact errors and rank.
7 Indices are zero-based and all tail values vanish beyond the diagonal length. -/
8 public section
9 set_option autoImplicit false
10 namespace KomorebiPaperVIII.SmallCore
11 open scoped BigOperators Matrix Classical
12 variable {d : ℕ}
13 def kept (σ : Fin d → ℝ) (k : ℕ) (i : Fin d) : ℝ := if i.val < k then σ i else 0
14 def discarded (σ : Fin d → ℝ) (k : ℕ) (i : Fin d) : ℝ := if i.val < k then 0 else σ i
15 noncomputable def diag (σ : Fin d → ℝ) : Matrix (Fin d) (Fin d) ℂ :=
16   Matrix.diagonal (fun i => (σ i : ℂ))
17 noncomputable def nextSingular (σ : Fin d → ℝ) (k : ℕ) : ℝ :=
18   if h : k < d then σ ⟨k,h⟩ else 0
19 noncomputable def tailEnergy (σ : Fin d → ℝ) (k : ℕ) : ℝ :=
20   ∑ i, (discarded σ k i)^2
21 noncomputable def rootKept (σ : Fin d → ℝ) (k : ℕ) : Matrix (Fin d) (Fin d) ℂ :=
22   diag (fun i => Real.sqrt (kept σ k i))
23 
24 theorem kept_nonneg (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i) (k : ℕ) (i : Fin d) :
25     0 ≤ kept σ k i := by unfold kept; split_ifs <;> first | exact hσ i | exact le_rfl
26 
27 theorem discarded_nonneg (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i) (k : ℕ) (i : Fin d) :
28     0 ≤ discarded σ k i := by unfold discarded; split_ifs <;> first | exact hσ i | exact le_rfl
29 
30 theorem diagonal_residual (σ : Fin d → ℝ) (k : ℕ) :
31     diag σ - diag (kept σ k) = diag (discarded σ k) := by
32   unfold diag
33   rw [Matrix.diagonal_sub]
34   congr 1
35   funext i
36   by_cases hi : i.val<k <;> simp [kept,discarded,hi]
37 
38 theorem rank_kept_le (σ : Fin d → ℝ) (k : ℕ) : (diag (kept σ k)).rank ≤ k := by
39   unfold diag
40   rw [Matrix.rank_diagonal]
41   let f : {i : Fin d // (kept σ k i : ℂ) ≠ 0} → Fin k := fun i =>
42     ⟨i.val.val,by
43       by_contra h
44       have he : kept σ k i.val = 0 := by simp [kept,h]
45       exact i.property (by rw [he]; rfl)⟩
46   have hf : Function.Injective f := by
47     intro i j he
48     apply Subtype.ext
49     apply Fin.ext
50     exact congrArg (fun x : Fin k => x.val) he
51   simpa only [Fintype.card_fin] using Fintype.card_le_of_injective f hf
52 
53 theorem rootKept_selfAdjoint (σ : Fin d → ℝ) (k : ℕ) :
54     (rootKept σ k)ᴴ = rootKept σ k := by
55   simp [rootKept,diag,Matrix.diagonal_conjTranspose]
56 
57 theorem rootKept_square (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i) (k : ℕ) :
58     rootKept σ k * rootKept σ k = diag (kept σ k) := by
59   unfold rootKept diag
60   rw [Matrix.diagonal_mul_diagonal]
61   congr 1
62   funext i
63   norm_cast
64   nlinarith [Real.sq_sqrt (kept_nonneg σ hσ k i)]
65 
66 theorem discarded_le_next (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i)
67     (hsort : Antitone σ) (k : ℕ) (i : Fin d) : discarded σ k i ≤ nextSingular σ k := by
68   by_cases hk : k<d
69   · simp only [nextSingular,hk]
70     by_cases hi : i.val<k
71     · simp only [discarded,hi,ite_true]; exact hσ _
72     · simp only [discarded,hi,ite_false]
73       exact hsort (by show k ≤ i.val; omega)
74   · have hi : i.val<k := by omega
75     simp [discarded,hi,nextSingular,hk]
76 
77 section Operator
78 open scoped Matrix.Norms.L2Operator
79 
80 theorem spectral_diagonal_tail (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i)
81     (hsort : Antitone σ) (k : ℕ) :
82     spectralNorm (diag (discarded σ k)) = nextSingular σ k := by
83   unfold spectralNorm diag
84   rw [Matrix.l2_opNorm_diagonal]
85   have hn : 0 ≤ nextSingular σ k := by
86     by_cases hk : k<d
87     · simpa [nextSingular,hk] using hσ ⟨k,hk⟩
88     · simp [nextSingular,hk]
89   apply le_antisymm
90   · apply (pi_norm_le_iff_of_nonneg hn).mpr
91     intro i
92     simpa only [Complex.norm_real,Real.norm_eq_abs,
93       abs_of_nonneg (discarded_nonneg σ hσ k i)] using discarded_le_next σ hσ hsort k i
94   · by_cases hk : k<d
95     · have hb := norm_le_pi_norm (fun i : Fin d => (discarded σ k i : ℂ)) ⟨k,hk⟩
96       simpa [nextSingular,hk,discarded,Complex.norm_real,Real.norm_eq_abs,
97         abs_of_nonneg (hσ ⟨k,hk⟩)] using hb
98     · simp only [nextSingular,hk]; positivity
99 end Operator
100 
101 section Frobenius
102 open scoped Matrix.Norms.Frobenius
103 
104 theorem frobenius_diagonal_tail (σ : Fin d → ℝ) (k : ℕ) :
105     frobeniusNorm (diag (discarded σ k))^2 = tailEnergy σ k := by
106   unfold frobeniusNorm diag tailEnergy
107   rw [Matrix.frobenius_norm_diagonal,EuclideanSpace.norm_sq_eq]
108   simp [Complex.norm_real,Real.norm_eq_abs,sq_abs]
109 end Frobenius
110 end KomorebiPaperVIII.SmallCore
111 
112 -- SIXTH AXIOM AUDITS
113 #print axioms KomorebiPaperVIII.SmallCore.kept_nonneg
114 #print axioms KomorebiPaperVIII.SmallCore.discarded_nonneg
115 #print axioms KomorebiPaperVIII.SmallCore.diagonal_residual
116 #print axioms KomorebiPaperVIII.SmallCore.rank_kept_le
117 #print axioms KomorebiPaperVIII.SmallCore.rootKept_selfAdjoint
118 #print axioms KomorebiPaperVIII.SmallCore.rootKept_square
119 #print axioms KomorebiPaperVIII.SmallCore.discarded_le_next
120 #print axioms KomorebiPaperVIII.SmallCore.spectral_diagonal_tail
121 #print axioms KomorebiPaperVIII.SmallCore.frobenius_diagonal_tail
122 #print axioms KomorebiPaperVIII.SmallCore.diag
123 #print axioms KomorebiPaperVIII.SmallCore.discarded
124 #print axioms KomorebiPaperVIII.SmallCore.kept
125 #print axioms KomorebiPaperVIII.SmallCore.nextSingular
126 #print axioms KomorebiPaperVIII.SmallCore.rootKept
127 #print axioms KomorebiPaperVIII.SmallCore.tailEnergy

Back to source controls