SpectralSharpness.lean

1 import KomorebiLSM.SpectralPseudoinverse
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Spectral
5 open Komorebi.LSM.Identification
6 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
8 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
9 
10 theorem image_basis_norm (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E)) :
11     ‖A (rightBasis A i)‖ = A.singularValues i := by
12   have h := image_inner A (rightBasis A i) i
13   simp only [real_inner_self_eq_norm_sq, (rightBasis A).norm_eq_one, one_pow, mul_one] at h
14   nlinarith [norm_nonneg (A (rightBasis A i)), A.singularValues_nonneg i]
15 
16 theorem positive_mode_orthogonal (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E))
17     (hi : 0 < A.singularValues i) : rightBasis A i ∈ A.kerᗮ := by
18   apply (A.ker.mem_orthogonal' _).mpr
19   intro y hy
20   have h := image_inner A y i
21   have hz : A y = 0 := hy
22   rw [hz, inner_zero_right] at h
23   exact (mul_eq_zero.mp h.symm).resolve_left (pow_ne_zero _ (ne_of_gt hi))
24 
25 theorem exists_unit_minimizer (A : E →ₗ[ℝ] F)
26     (hr : 0 < Module.finrank ℝ A.range) :
27     ∃ v : E, v ∈ A.kerᗮ ∧ ‖v‖ = 1 ∧ ‖A v‖ = leastPositive A := by
28   have hd := LinearMap.finrank_range_le A
29   let i : Fin (Module.finrank ℝ E) := ⟨Module.finrank ℝ A.range-1, by omega⟩
30   refine ⟨rightBasis A i, positive_mode_orthogonal A i (leastPositive_pos A hr),
31     (rightBasis A).norm_eq_one i, ?_⟩
32   exact image_basis_norm A i
33 
34 /-- Sharp operator norm for the actual orthogonal pseudoinverse. -/
35 theorem pinv_operator_norm_eq (A : E →L[ℝ] F)
36     (hr : 0 < Module.finrank ℝ A.toLinearMap.range) :
37     ‖pinvL A‖ = (leastPositive A.toLinearMap)⁻¹ := by
38   apply le_antisymm (pinv_operator_bound A hr)
39   obtain ⟨v,hv,hn,ha⟩ := exists_unit_minimizer A.toLinearMap hr
40   have he : pinvL A (A v) = v := by
41     change pinv A.toLinearMap (A.toLinearMap v) = v
42     rw [pinv_apply_image]
43     exact A.toLinearMap.kerᗮ.starProjection_eq_self_iff.mpr hv
44   change ‖A v‖ = leastPositive A.toLinearMap at ha
45   have h := (pinvL A).le_opNorm (A v)
46   rw [he, hn, ha] at h
47   rw [inv_eq_one_div]
48   exact (div_le_iff₀ (leastPositive_pos A.toLinearMap hr)).mpr h
49 
50 /-- Restricting the pseudoinverse to its actual range keeps the sharp norm. -/
51 theorem rangeInverse_norm_eq (A : E →L[ℝ] F)
52     (hr : 0 < Module.finrank ℝ A.toLinearMap.range) :
53     ‖rangeInverse A‖ = (leastPositive A.toLinearMap)⁻¹ := by
54   apply le_antisymm (rangeInverse_bound A hr)
55   obtain ⟨v,hv,hn,ha⟩ := exists_unit_minimizer A.toLinearMap hr
56   let y : A.toLinearMap.range := A.toLinearMap.rangeRestrict v
57   have he : rangeInverse A y = v := by
58     change pinv A.toLinearMap (A.toLinearMap v) = v
59     rw [pinv_apply_image]
60     exact A.toLinearMap.kerᗮ.starProjection_eq_self_iff.mpr hv
61   have hy : ‖y‖ = leastPositive A.toLinearMap := ha
62   have h := (rangeInverse A).le_opNorm y
63   rw [he, hn, hy] at h
64   rw [inv_eq_one_div]
65   exact (div_le_iff₀ (leastPositive_pos A.toLinearMap hr)).mpr h
66 
67 end Komorebi.LSM.Spectral

Back to source controls