Block12Examples.lean

1 import KomorebiLSM.NoisySubspaceResidual
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Block12Examples
5 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [FiniteDimensional ℝ E]
7 
8 theorem zero_residual_equal_rank (P Q : Submodule ℝ E)
9     (hres : ∀ x : P, (x:E) = Q.starProjection x)
10     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
11     P.starProjection = Q.starProjection := by
12   have h := OneSidedSubspace.projection_gap P Q 0 (by norm_num) (by norm_num)
13     (by intro x; rw [← hres x]; simp) hdim
14   exact sub_eq_zero.mp (norm_eq_zero.mp (le_antisymm h (norm_nonneg _)))
15 
16 theorem unequal_rank_zero_one_sided :
17     ∀ x : (⊥ : Submodule ℝ ℝ), ‖(x:ℝ)-(⊤ : Submodule ℝ ℝ).starProjection x‖ = 0 := by
18   intro x
19   simp [Submodule.starProjection_top]
20 
21 theorem unequal_rank_full_gap_one :
22     ‖(⊥ : Submodule ℝ ℝ).starProjection-(⊤ : Submodule ℝ ℝ).starProjection‖ = 1 := by
23   simp [Submodule.starProjection_top]
24 
25 theorem quarter_noise_gap (P Q : Submodule ℝ E)
26     (hres : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ (1/2:ℝ)*‖x‖)
27     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
28     ‖P.starProjection-Q.starProjection‖ ≤ (1/2:ℝ) :=
29   OneSidedSubspace.projection_gap P Q (1/2) (by norm_num) (by norm_num) hres hdim
30 
31 end Komorebi.LSM.Block12Examples

Back to source controls