FrobeniusOptimality.lean

1 module
2 public import KernelFrame
3 public import DiagonalTruncation
4 import all SmallCoreNorms
5 import all KernelFrame
6 import all DiagonalTruncation
7 import all SmallCoreTransfer
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Frobenius low-rank lower bound proved from kernel weights.
10 No Eckart--Young optimality assumption is used in this module. -/
11 public section
12 set_option autoImplicit false
13 namespace KomorebiPaperVIII.SmallCore
14 open scoped BigOperators Matrix Classical
15 variable {d : ℕ}
16 
17 theorem tail_indicator_sum (k : ℕ) (hk : k ≤ d) :
18     (∑ i : Fin d, if i.val < k then (0:ℝ) else 1) = (d-k : ℕ) := by
19   have htop : (∑ i : Fin d, if i.val < k then (1:ℝ) else 0) = k := by
20     rw [←Finset.natCast_card_filter]
21     simp [Fin.card_filter_val_lt,Nat.min_eq_right hk]
22   have hsplit : (∑ i : Fin d, if i.val < k then (1:ℝ) else 0) +
23       (∑ i : Fin d, if i.val < k then (0:ℝ) else 1) = d := by
24     rw [←Finset.sum_add_distrib]
25     have he : (fun i : Fin d => (if i.val<k then (1:ℝ) else 0)+
26         (if i.val<k then (0:ℝ) else 1)) = fun _ => (1:ℝ) := by
27       funext i; split_ifs <;> norm_num
28     rw [he]
29     simp
30   rw [htop] at hsplit
31   rw [Nat.cast_sub hk]
32   linarith
33 
34 /-- A decreasing nonnegative cost is minimized by placing the available mass at the tail. -/
35 theorem weighted_tail_lower (a w : Fin d → ℝ) (ha : ∀ i, 0 ≤ a i)
36     (hsort : Antitone a) (hw0 : ∀ i, 0 ≤ w i) (hw1 : ∀ i, w i ≤ 1)
37     (k : ℕ) (hw : (d-k : ℕ) ≤ ∑ i,w i) :
38     (∑ i, if i.val<k then (0:ℝ) else a i) ≤ ∑ i, a i*w i := by
39   by_cases hk : k<d
40   · let μ := a ⟨k,hk⟩
41     have hμ : 0 ≤ μ := ha _
42     have hp : ∀ i : Fin d,
43         (if i.val<k then 0 else a i) + μ*(w i-(if i.val<k then 0 else 1)) ≤ a i*w i := by
44       intro i
45       by_cases hi : i.val<k
46       · have hle : μ ≤ a i := hsort (by show i.val ≤ k; omega)
47         simp only [hi,ite_true,zero_add,sub_zero]
48         exact mul_le_mul_of_nonneg_right hle (hw0 i)
49       · have hle : a i ≤ μ := hsort (by show k ≤ i.val; omega)
50         simp only [hi,ite_false]
51         nlinarith [mul_nonneg (sub_nonneg.mpr hle) (sub_nonneg.mpr (hw1 i))]
52     have hs := Finset.sum_le_sum (fun i (_ : i ∈ (Finset.univ : Finset (Fin d))) => hp i)
53     simp only [Finset.sum_add_distrib] at hs
54     have ht := tail_indicator_sum (d:=d) k hk.le
55     have hz : 0 ≤ μ*((∑ i,w i)-(d-k : ℕ)) := mul_nonneg hμ (sub_nonneg.mpr hw)
56     rw [←Finset.mul_sum,Finset.sum_sub_distrib,ht] at hs
57     linarith
58   · have he : ∀ i : Fin d, i.val<k := fun i => by omega
59     simp only [he,ite_true,Finset.sum_const_zero]
60     exact Finset.sum_nonneg (fun i _ => mul_nonneg (ha i) (hw0 i))
61 
62 section Frobenius
63 open scoped Matrix.Norms.Frobenius
64 
65 theorem diagonal_frame_energy {r : Type*} [Fintype r] (σ : Fin d → ℝ)
66     (Q : Matrix (Fin d) r ℂ) :
67     frobeniusNorm (diag σ * Q)^2 = ∑ i, σ i^2 * rowWeight Q i := by
68   unfold frobeniusNorm
69   rw [Matrix.frobenius_norm_def]
70   simp only [Real.rpow_two,←Real.sqrt_eq_rpow]
71   rw [Real.sq_sqrt (Finset.sum_nonneg (fun i _ => Finset.sum_nonneg
72     (fun j _ => sq_nonneg ‖(diag σ*Q) i j‖)))]
73   simp [diag,Matrix.diagonal_mul,mul_pow,Complex.norm_real,
74     Real.norm_eq_abs,sq_abs,rowWeight,Finset.mul_sum]
75 
76 theorem diagonal_frobenius_lower (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i)
77     (hsort : Antitone σ) (k : ℕ) (B : Matrix (Fin d) (Fin d) ℂ) (hB : B.rank≤k) :
78     tailEnergy σ k ≤ frobeniusNorm (diag σ-B)^2 := by
79   let Q := kernelFrame B
80   have hQ : Qᴴ*Q=1 := kernelFrame_isometry B
81   have hw : (d-k : ℕ) ≤ ∑ i,rowWeight Q i := by
82     rw [rowWeight_sum Q hQ]
83     simp only [Fintype.card_fin]
84     have hn := kernel_rank_nullity B
85     simp only [Fintype.card_fin] at hn
86     exact_mod_cast (by omega : d-k ≤ kernelDim B)
87   have hsort2 : Antitone (fun i => σ i^2) := by
88     intro i j hij
89     have hle := hsort hij
90     nlinarith [hσ i,hσ j]
91   have hl := weighted_tail_lower (fun i => σ i^2) (rowWeight Q)
92     (fun i => sq_nonneg _) hsort2 (rowWeight_nonneg Q) (rowWeight_le_one Q hQ) k hw
93   have he : tailEnergy σ k = ∑ i, if i.val<k then (0:ℝ) else σ i^2 := by
94     unfold tailEnergy discarded
95     apply Finset.sum_congr rfl
96     intro i _
97     split_ifs <;> simp
98   rw [←he,←diagonal_frame_energy σ Q] at hl
99   have hc := frobenius_right_compress_le Q hQ (diag σ-B)
100   have hbq : (diag σ-B)*Q=diag σ*Q := by
101     rw [Matrix.sub_mul,mul_kernelFrame,sub_zero]
102   rw [hbq] at hc
103   unfold frobeniusNorm at hl ⊢
104   nlinarith [norm_nonneg (diag σ*Q),norm_nonneg (diag σ-B)]
105 
106 theorem diagonal_frobenius_best (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i)
107     (hsort : Antitone σ) (k : ℕ) :
108     BestRank frobeniusNorm (diag σ) (diag (kept σ k)) k := by
109   refine ⟨rank_kept_le σ k,fun B hB => ?_⟩
110   have hl := diagonal_frobenius_lower σ hσ hsort k B hB
111   have he := frobenius_diagonal_tail σ k
112   rw [←diagonal_residual] at he
113   unfold frobeniusNorm at *
114   nlinarith [norm_nonneg (diag σ-diag (kept σ k)),norm_nonneg (diag σ-B)]
115 end Frobenius
116 end KomorebiPaperVIII.SmallCore
117 
118 -- SIXTH AXIOM AUDITS
119 #print axioms KomorebiPaperVIII.SmallCore.tail_indicator_sum
120 #print axioms KomorebiPaperVIII.SmallCore.weighted_tail_lower
121 #print axioms KomorebiPaperVIII.SmallCore.diagonal_frame_energy
122 #print axioms KomorebiPaperVIII.SmallCore.diagonal_frobenius_lower
123 #print axioms KomorebiPaperVIII.SmallCore.diagonal_frobenius_best

Back to source controls