SubspaceCoordinates.lean

1 import KomorebiLSM.IdentificationBound
2 import Mathlib.Analysis.InnerProductSpace.SingularValues
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.SubspaceCoordinates
6 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [FiniteDimensional ℝ E]
8 
9 /-- Coordinates in the estimated subspace, before a choice of orthonormal basis. -/
10 noncomputable def project (P Q : Submodule ℝ E) : P →L[ℝ] Q :=
11   Q.orthogonalProjectionOnto.comp P.subtypeL
12 
13 /-- This lemma takes the projection gap as a hypothesis. It does not establish
14 the singular-subspace perturbation bound from noisy data. -/
15 theorem coordinate_lower (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
16     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) (x : P) :
17     Real.sqrt (1-δ^2) * ‖x‖ ≤ ‖project P Q x‖ := by
18   have hres : ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖ := by
19     have h := (P.starProjection-Q.starProjection).le_opNorm (x:E)
20     rw [sub_apply, P.starProjection_eq_self_iff.mpr x.property] at h
21     exact h.trans (mul_le_mul_of_nonneg_right hgap (norm_nonneg _))
22   have hp := Q.norm_sq_eq_add_norm_sq_starProjection (x:E)
23   have horth : Qᗮ.starProjection (x:E) = (x:E)-Q.starProjection x := by
24     have h := Q.starProjection_add_starProjection_orthogonal (x:E)
25     exact eq_sub_of_add_eq' h
26   rw [horth] at hp
27   have hs : 0 ≤ 1-δ^2 := by nlinarith
28   have hsqrt := Real.sq_sqrt hs
29   have hn : ‖project P Q x‖ = ‖Q.starProjection (x:E)‖ := rfl
30   rw [hn]
31   have hres0 := norm_nonneg ((x:E)-Q.starProjection x)
32   have hsq : ‖(x:E)-Q.starProjection x‖^2 ≤ (δ*‖x‖)^2 := by nlinarith
33   have hx : ‖(x:E)‖ = ‖x‖ := rfl
34   rw [hx] at hp
35   have hprod : (Real.sqrt (1-δ^2)*‖x‖)^2 = (1-δ^2)*‖x‖^2 := by
36     rw [mul_pow, hsqrt]
37   nlinarith [Real.sqrt_nonneg (1-δ^2), norm_nonneg (Q.starProjection (x:E)), norm_nonneg x]
38 
39 theorem coordinate_injective (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
40     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) :
41     Function.Injective (project P Q) := by
42   apply (project P Q).toLinearMap.ker_eq_bot.mp
43   apply le_antisymm _ bot_le
44   intro x hx
45   have hz : project P Q x = 0 := hx
46   have hl := coordinate_lower P Q δ hδ hsmall hgap x
47   rw [hz, norm_zero] at hl
48   have hp : 0 < Real.sqrt (1-δ^2) := Real.sqrt_pos.mpr (by nlinarith)
49   have hnorm : ‖x‖ = 0 := by nlinarith [norm_nonneg x]
50   simp [norm_eq_zero.mp hnorm]
51 
52 noncomputable def coordinateEquiv (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
53     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ)
54     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) : P ≃L[ℝ] Q :=
55   (LinearEquiv.ofBijective (project P Q).toLinearMap
56     ⟨coordinate_injective P Q δ hδ hsmall hgap,
57       (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp
58         (coordinate_injective P Q δ hδ hsmall hgap)⟩).toContinuousLinearEquiv
59 
60 theorem coordinate_inverse_bound (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
61     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ)
62     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
63     ‖(coordinateEquiv P Q δ hδ hsmall hgap hdim).symm.toContinuousLinearMap‖ ≤
64       (Real.sqrt (1-δ^2))⁻¹ := by
65   have hp : 0 < Real.sqrt (1-δ^2) := Real.sqrt_pos.mpr (by nlinarith)
66   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr hp.le)
67   intro y
68   have h := coordinate_lower P Q δ hδ hsmall hgap
69     ((coordinateEquiv P Q δ hδ hsmall hgap hdim).symm y)
70   have he : project P Q ((coordinateEquiv P Q δ hδ hsmall hgap hdim).symm y) = y :=
71     (coordinateEquiv P Q δ hδ hsmall hgap hdim).apply_symm_apply y
72   rw [he] at h
73   rw [inv_mul_eq_div]
74   exact (le_div_iff₀ hp).mpr (by simpa [mul_comm] using h)
75 
76 end Komorebi.LSM.SubspaceCoordinates

Back to source controls