SpectralLowerBound.lean

1 import KomorebiLSM.SubspaceCoordinates
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Spectral
5 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
7 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
8 
9 /-- Ordered orthonormal eigenbasis of the actual right Gram operator. -/
10 noncomputable def rightBasis (A : E →ₗ[ℝ] F) :
11     OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E :=
12   A.isSymmetric_adjoint_comp_self.eigenvectorBasis rfl
13 
14 theorem image_inner (A : E →ₗ[ℝ] F) (x : E) (i : Fin (Module.finrank ℝ E)) :
15     inner ℝ (A (rightBasis A i)) (A x) =
16       A.singularValues i ^ 2 * inner ℝ (rightBasis A i) x := by
17   have hg := A.isSymmetric_adjoint_comp_self.apply_eigenvectorBasis rfl i
18   change A.adjoint (A (rightBasis A i)) = _ at hg
19   rw [← A.adjoint_inner_left, hg]
20   rw [← A.sq_singularValues_fin rfl i]
21   simp [inner_smul_left, rightBasis]
22 
23 theorem image_norm_sq (A : E →ₗ[ℝ] F) (x : E) :
24     ‖A x‖^2 = ∑ i : Fin (Module.finrank ℝ E),
25       A.singularValues i ^ 2 * (inner ℝ (rightBasis A i) x)^2 := by
26   calc
27     ‖A x‖^2 = inner ℝ x (A.adjoint (A x)) := by
28       rw [A.adjoint_inner_right]
29       simp
30     _ = ∑ i, inner ℝ x (rightBasis A i) *
31         inner ℝ (rightBasis A i) (A.adjoint (A x)) :=
32       ((rightBasis A).sum_inner_mul_inner x (A.adjoint (A x))).symm
33     _ = _ := by
34       apply Finset.sum_congr rfl
35       intro i _
36       rw [A.adjoint_inner_right, image_inner, real_inner_comm x]
37       ring
38 
39 theorem zero_mode_mem_kernel (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E))
40     (hz : A.singularValues i = 0) : rightBasis A i ∈ A.ker := by
41   have h := image_inner A (rightBasis A i) i
42   simp [hz] at h
43   exact h
44 
45 theorem tail_coordinate_zero (A : E →ₗ[ℝ] F) (x : E) (hx : x ∈ A.kerᗮ)
46     (i : Fin (Module.finrank ℝ E)) (hi : Module.finrank ℝ A.range ≤ i) :
47     inner ℝ (rightBasis A i) x = 0 :=
48   A.ker.inner_right_of_mem_orthogonal
49     (zero_mode_mem_kernel A i (A.singularValues_eq_zero_iff_le_finrank_range.mpr hi)) hx
50 
51 /-- The actual smallest positive singular value, at zero-based index rank−1. -/
52 noncomputable def leastPositive (A : E →ₗ[ℝ] F) : ℝ :=
53   A.singularValues (Module.finrank ℝ A.range - 1)
54 
55 theorem leastPositive_pos (A : E →ₗ[ℝ] F) (hr : 0 < Module.finrank ℝ A.range) :
56     0 < leastPositive A := by
57   apply A.singularValues_pos_iff_lt_finrank_range.mpr
58   omega
59 
60 theorem lower_on_kernel_orthogonal (A : E →ₗ[ℝ] F)
61     (x : E) (hx : x ∈ A.kerᗮ) : leastPositive A * ‖x‖ ≤ ‖A x‖ := by
62   have hs : 0 ≤ leastPositive A := A.singularValues_nonneg _
63   have hsum : (leastPositive A)^2 * ‖x‖^2 ≤ ‖A x‖^2 := by
64     rw [image_norm_sq, ← (rightBasis A).sum_sq_inner_right x, Finset.mul_sum]
65     apply Finset.sum_le_sum
66     intro i _
67     by_cases hi : (i:ℕ) < Module.finrank ℝ A.range
68     · have hle : leastPositive A ≤ A.singularValues i :=
69         A.singularValues_antitone (by omega)
70       exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hs hle 2) (sq_nonneg _)
71     · rw [tail_coordinate_zero A x hx i (by omega)]
72       simp
73   have hp : (leastPositive A * ‖x‖)^2 = (leastPositive A)^2 * ‖x‖^2 := mul_pow _ _ 2
74   nlinarith [mul_nonneg hs (norm_nonneg x), norm_nonneg (A x)]
75 
76 end Komorebi.LSM.Spectral

Back to source controls