NoisySubspaceResidual.lean

1 import KomorebiLSM.OneSidedSubspace
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.OneSidedSubspace
5 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
7 
8 /-- Transfer an observed tail bound to the true operator using its actual error. -/
9 theorem true_residual (Q : Submodule ℝ E) (X N : F →L[ℝ] E)
10     (η ε : ℝ) (htail : ‖Qᗮ.starProjection.comp (X+N)‖ ≤ η)
11     (hnoise : ‖N‖ ≤ ε) (u : F) :
12     ‖Qᗮ.starProjection (X u)‖ ≤ (η+ε)*‖u‖ := by
13   have ht := (Qᗮ.starProjection.comp (X+N)).le_opNorm u
14   have hn := N.le_opNorm u
15   have hp := Qᗮ.norm_starProjection_apply_le (N u)
16   have he : Qᗮ.starProjection (X u) =
17       Qᗮ.starProjection ((X+N) u)-Qᗮ.starProjection (N u) := by
18     rw [add_apply, map_add]
19     abel
20   rw [he]
21   calc
22     _ ≤ ‖Qᗮ.starProjection ((X+N) u)‖+‖Qᗮ.starProjection (N u)‖ := norm_sub_le _ _
23     _ ≤ η*‖u‖+ε*‖u‖ := add_le_add
24       (ht.trans (mul_le_mul_of_nonneg_right htail (norm_nonneg u)))
25       (hp.trans (hn.trans (mul_le_mul_of_nonneg_right hnoise (norm_nonneg u))))
26     _ = _ := by ring
27 
28 /-- A bounded right inverse on the true subspace transfers the data residual.
29 Its norm estimate remains an explicit premise, separate from singular values. -/
30 theorem residual_on_range (P Q : Submodule ℝ E) (X N : F →L[ℝ] E)
31     (R : P →L[ℝ] F) (η ε κ : ℝ) (hη : 0 ≤ η) (hε : 0 ≤ ε)
32     (htail : ‖Qᗮ.starProjection.comp (X+N)‖ ≤ η) (hnoise : ‖N‖ ≤ ε)
33     (hR : ‖R‖ ≤ κ) (hright : ∀ x : P, X (R x) = (x:E)) (x : P) :
34     ‖(x:E)-Q.starProjection x‖ ≤ ((η+ε)*κ)*‖x‖ := by
35   have he : Qᗮ.starProjection (x:E) = (x:E)-Q.starProjection x :=
36     eq_sub_of_add_eq' (Q.starProjection_add_starProjection_orthogonal (x:E))
37   rw [← he, ← hright x]
38   have h := true_residual Q X N η ε htail hnoise (R x)
39   have hr := (R.le_opNorm x).trans (mul_le_mul_of_nonneg_right hR (norm_nonneg x))
40   exact h.trans (by simpa [mul_assoc] using
41     mul_le_mul_of_nonneg_left hr (add_nonneg hη hε))
42 
43 /-- Conditional noisy-table gap: the tail and inverse estimates are inputs. -/
44 theorem noisy_projection_gap (P Q : Submodule ℝ E) (X N : F →L[ℝ] E)
45     (R : P →L[ℝ] F) (η ε κ : ℝ) (hη : 0 ≤ η) (hε : 0 ≤ ε) (hκ : 0 ≤ κ)
46     (htail : ‖Qᗮ.starProjection.comp (X+N)‖ ≤ η) (hnoise : ‖N‖ ≤ ε)
47     (hR : ‖R‖ ≤ κ) (hright : ∀ x : P, X (R x) = (x:E))
48     (hsmall : (η+ε)*κ < 1) (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
49     ‖P.starProjection-Q.starProjection‖ ≤ (η+ε)*κ :=
50   projection_gap P Q _ (mul_nonneg (add_nonneg hη hε) hκ) hsmall
51     (residual_on_range P Q X N R η ε κ hη hε htail hnoise hR hright) hdim
52 
53 /-- The manuscript's constant follows once the spectral tail and inverse bounds
54 are supplied; this theorem does not infer either spectral premise. -/
55 theorem two_epsilon_gap (P Q : Submodule ℝ E) (X N : F →L[ℝ] E)
56     (R : P →L[ℝ] F) (ε s : ℝ) (hε : 0 ≤ ε) (hs : 0 < s) (hsmall : ε < s/2)
57     (htail : ‖Qᗮ.starProjection.comp (X+N)‖ ≤ ε) (hnoise : ‖N‖ ≤ ε)
58     (hR : ‖R‖ ≤ s⁻¹) (hright : ∀ x : P, X (R x) = (x:E))
59     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
60     ‖P.starProjection-Q.starProjection‖ ≤ 2*ε/s ∧ 2*ε/s < 1 := by
61   have he : (ε+ε)*s⁻¹ = 2*ε/s := by ring
62   have hm : 2*ε/s < 1 := (div_lt_one hs).mpr (by linarith)
63   refine ⟨?_,hm⟩
64   rw [← he]
65   exact noisy_projection_gap P Q X N R ε ε s⁻¹ hε hε (inv_nonneg.mpr hs.le)
66     htail hnoise hR hright (by rwa [he]) hdim
67 
68 end Komorebi.LSM.OneSidedSubspace

Back to source controls