IdentificationBound.lean

1 import KomorebiLSM.Pseudoinverse
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Identification
5 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
7 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
8 
9 noncomputable def pinvL (A : E →L[ℝ] F) : F →L[ℝ] E := (pinv A.toLinearMap).toContinuousLinearMap
10 
11 /-- Variational smallest row singular value, using nonzero vectors to avoid normalization choices. -/
12 noncomputable def rowGain (A : E →L[ℝ] F) : ℝ :=
13   sInf {r : ℝ | ∃ v : F, v ≠ 0 ∧ r = ‖A.adjoint v‖ / ‖v‖}
14 
15 theorem rowGain_variational_unit (A : E →L[ℝ] F) :
16     rowGain A = sInf {r : ℝ | ∃ v : F, ‖v‖ = 1 ∧ r = ‖A.adjoint v‖} := by
17   unfold rowGain
18   congr 1
19   ext r
20   constructor
21   · rintro ⟨v,hv,rfl⟩
22     have hn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv
23     refine ⟨‖v‖⁻¹ • v, ?_, ?_⟩
24     · rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg (norm_nonneg v), inv_mul_cancel₀ hn]
25     · rw [map_smul, norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg (norm_nonneg v)]
26       exact div_eq_inv_mul _ _
27   · rintro ⟨v,hv,rfl⟩
28     refine ⟨v, ?_, ?_⟩
29     · intro hz; simp [hz] at hv
30     · rw [hv, div_one]
31 
32 theorem rowGain_lower (A : E →L[ℝ] F) (v : F) : rowGain A * ‖v‖ ≤ ‖A.adjoint v‖ := by
33   by_cases hv : v = 0
34   · simp [hv]
35   · have hn : 0 < ‖v‖ := norm_pos_iff.mpr hv
36     have hb : BddBelow {r : ℝ | ∃ w : F, w ≠ 0 ∧ r = ‖A.adjoint w‖ / ‖w‖} := by
37       refine ⟨0, ?_⟩
38       rintro r ⟨w,_,rfl⟩
39       exact div_nonneg (norm_nonneg _) (norm_nonneg _)
40     have hi := csInf_le hb (show ‖A.adjoint v‖ / ‖v‖ ∈
41       {r : ℝ | ∃ w : F, w ≠ 0 ∧ r = ‖A.adjoint w‖ / ‖w‖} from ⟨v,hv,rfl⟩)
42     exact (le_div_iff₀ hn).mp hi
43 
44 theorem rowGain_perturbation (A E' : E →L[ℝ] F) (v : F) :
45     (rowGain A - ‖E'‖) * ‖v‖ ≤ ‖(A+E').adjoint v‖ := by
46   have h1 := rowGain_lower A v
47   have h2 := E'.adjoint.le_opNorm v
48   have h3 : ‖A.adjoint v‖ ≤ ‖(A+E').adjoint v‖ + ‖E'.adjoint v‖ := by
49     have he : A.adjoint v = (A+E').adjoint v - E'.adjoint v := by simp
50     rw [he]
51     exact norm_sub_le _ _
52   simpa using (by nlinarith :
53     (rowGain A - ‖E'.adjoint‖) * ‖v‖ ≤ ‖(A+E').adjoint v‖)
54 
55 theorem surjective_of_adjoint_lower (A : E →L[ℝ] F) (c : ℝ) (hc : 0 < c)
56     (hl : ∀ v, c * ‖v‖ ≤ ‖A.adjoint v‖) : Function.Surjective A := by
57   have hk : A.toLinearMap.adjoint.ker = ⊥ := by
58     apply le_antisymm _ bot_le
59     intro v hv
60     have h := hl v
61     have hz : A.adjoint v = 0 := hv
62     rw [hz, norm_zero] at h
63     have hv0 : v = 0 := norm_eq_zero.mp (by nlinarith [norm_nonneg v])
64     simp [hv0]
65   have ho : A.toLinearMap.rangeᗮ = ⊥ := by rw [LinearMap.orthogonal_range, hk]
66   have hr : A.toLinearMap.range = ⊤ := by
67     have he := congrArg (fun W : Submodule ℝ F => Wᗮ) ho
68     simpa using he
69   exact LinearMap.range_eq_top.mp hr
70 
71 theorem pinvL_right (A : E →L[ℝ] F) (hs : Function.Surjective A) (y : F) :
72     A (pinvL A y) = y := by
73   change A.toLinearMap (pinv A.toLinearMap y) = y
74   rw [apply_pinv]
75   exact A.toLinearMap.range.starProjection_eq_self_iff.mpr (hs y)
76 
77 theorem pinvL_bound (A : E →L[ℝ] F) (c : ℝ) (hc : 0 < c)
78     (hl : ∀ v, c * ‖v‖ ≤ ‖A.adjoint v‖) : ‖pinvL A‖ ≤ c⁻¹ := by
79   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr hc.le)
80   intro y
81   have hm := pinv_apply_mem A.toLinearMap y
82   rw [LinearMap.orthogonal_ker] at hm
83   obtain ⟨v,hv⟩ := hm
84   have hv' : A.adjoint v = pinvL A y := hv
85   have he : inner ℝ (pinvL A y) (pinvL A y) = inner ℝ v y := by
86     nth_rw 1 [← hv']
87     rw [ContinuousLinearMap.adjoint_inner_left, pinvL_right A (surjective_of_adjoint_lower A c hc hl)]
88   have hi := real_inner_le_norm v y
89   rw [real_inner_self_eq_norm_sq] at he
90   have hh := hl v
91   rw [hv'] at hh
92   have hn : c * ‖pinvL A y‖ ≤ ‖y‖ := by
93     by_cases hz : ‖pinvL A y‖ = 0
94     · simp [hz]
95     · have hp : 0 < ‖pinvL A y‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
96       have hm := mul_le_mul_of_nonneg_right hi hc.le
97       have hm2 := mul_le_mul_of_nonneg_right hh (norm_nonneg y)
98       nlinarith
99   rw [inv_mul_eq_div]
100   exact (le_div_iff₀ hc).mpr (by nlinarith)
101 
102 theorem noisy_identification_identity (A R E' F' : E →L[ℝ] F) (B : F →L[ℝ] F)
103     (hE : ‖E'‖ < rowGain A) :
104     ((B.comp A + R + F').comp (pinvL (A+E'))) - B =
105       (R + F' - B.comp E').comp (pinvL (A+E')) := by
106   have hs := surjective_of_adjoint_lower (A+E') (rowGain A - ‖E'‖)
107     (sub_pos.mpr hE) (rowGain_perturbation A E')
108   apply ContinuousLinearMap.ext
109   intro y
110   have he := pinvL_right (A+E') hs y
111   simp only [add_apply] at he
112   have hb := congrArg B he
113   simp only [map_add] at hb
114   simp only [sub_apply, ContinuousLinearMap.comp_apply,
115     add_apply]
116   rw [← hb]
117   abel
118 
119 theorem noisy_identification_bound (A R E' F' : E →L[ℝ] F) (B : F →L[ℝ] F)
120     (hE : ‖E'‖ < rowGain A) :
121     ‖((B.comp A + R + F').comp (pinvL (A+E'))) - B‖ ≤
122       (‖R‖ + ‖F'‖ + ‖B‖ * ‖E'‖) / (rowGain A - ‖E'‖) := by
123   rw [noisy_identification_identity A R E' F' B hE]
124   have hn : ‖R + F' - B.comp E'‖ ≤ ‖R‖ + ‖F'‖ + ‖B‖ * ‖E'‖ :=
125     (norm_sub_le _ _).trans (add_le_add (norm_add_le _ _) (ContinuousLinearMap.opNorm_comp_le _ _))
126   have hj := pinvL_bound (A+E') (rowGain A - ‖E'‖) (sub_pos.mpr hE)
127     (rowGain_perturbation A E')
128   calc
129     _ ≤ ‖R + F' - B.comp E'‖ * ‖pinvL (A+E')‖ := ContinuousLinearMap.opNorm_comp_le _ _
130     _ ≤ (‖R‖ + ‖F'‖ + ‖B‖ * ‖E'‖) * (rowGain A - ‖E'‖)⁻¹ :=
131       mul_le_mul hn hj (norm_nonneg _) (by positivity)
132     _ = _ := div_eq_mul_inv _ _ |>.symm
133 end Komorebi.LSM.Identification

Back to source controls