OneSidedSubspace.lean

1 import KomorebiLSM.SubspaceCoordinates
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.OneSidedSubspace
5 open Komorebi.LSM.SubspaceCoordinates
6 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [FiniteDimensional ℝ E]
8 
9 theorem coordinate_lower (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
10     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖) (x : P) :
11     Real.sqrt (1-δ^2) * ‖x‖ ≤ ‖project P Q x‖ := by
12   have hres := hgap x
13   have hp := Q.norm_sq_eq_add_norm_sq_starProjection (x:E)
14   have horth : Qᗮ.starProjection (x:E) = (x:E)-Q.starProjection x := by
15     have h := Q.starProjection_add_starProjection_orthogonal (x:E)
16     exact eq_sub_of_add_eq' h
17   rw [horth] at hp
18   have hs : 0 ≤ 1-δ^2 := by nlinarith
19   have hsqrt := Real.sq_sqrt hs
20   have hn : ‖project P Q x‖ = ‖Q.starProjection (x:E)‖ := rfl
21   rw [hn]
22   have hres0 := norm_nonneg ((x:E)-Q.starProjection x)
23   have hsq : ‖(x:E)-Q.starProjection x‖^2 ≤ (δ*‖x‖)^2 := by nlinarith
24   have hx : ‖(x:E)‖ = ‖x‖ := rfl
25   rw [hx] at hp
26   have hprod : (Real.sqrt (1-δ^2)*‖x‖)^2 = (1-δ^2)*‖x‖^2 := by
27     rw [mul_pow, hsqrt]
28   nlinarith [Real.sqrt_nonneg (1-δ^2), norm_nonneg (Q.starProjection (x:E)), norm_nonneg x]
29 
30 theorem coordinate_injective (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
31     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖) :
32     Function.Injective (project P Q) := by
33   apply (project P Q).toLinearMap.ker_eq_bot.mp
34   apply le_antisymm _ bot_le
35   intro x hx
36   have hz : project P Q x = 0 := hx
37   have hl := coordinate_lower P Q δ hδ hsmall hgap x
38   rw [hz, norm_zero] at hl
39   have hp : 0 < Real.sqrt (1-δ^2) := Real.sqrt_pos.mpr (by nlinarith)
40   have hnorm : ‖x‖ = 0 := by nlinarith [norm_nonneg x]
41   simp [norm_eq_zero.mp hnorm]
42 
43 noncomputable def coordinateEquiv (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
44     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
45     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) : P ≃L[ℝ] Q :=
46   (LinearEquiv.ofBijective (project P Q).toLinearMap
47     ⟨coordinate_injective P Q δ hδ hsmall hgap,
48       (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp
49         (coordinate_injective P Q δ hδ hsmall hgap)⟩).toContinuousLinearEquiv
50 
51 theorem coordinate_inverse_bound (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
52     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
53     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
54     ‖(coordinateEquiv P Q δ hδ hsmall hgap hdim).symm.toContinuousLinearMap‖ ≤
55       (Real.sqrt (1-δ^2))⁻¹ := by
56   have hp : 0 < Real.sqrt (1-δ^2) := Real.sqrt_pos.mpr (by nlinarith)
57   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr hp.le)
58   intro y
59   have h := coordinate_lower P Q δ hδ hsmall hgap
60     ((coordinateEquiv P Q δ hδ hsmall hgap hdim).symm y)
61   have he : project P Q ((coordinateEquiv P Q δ hδ hsmall hgap hdim).symm y) = y :=
62     (coordinateEquiv P Q δ hδ hsmall hgap hdim).apply_symm_apply y
63   rw [he] at h
64   rw [inv_mul_eq_div]
65   exact (le_div_iff₀ hp).mpr (by simpa [mul_comm] using h)
66 
67 theorem reverse_coordinate_lower (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
68     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
69     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) (y : Q) :
70     Real.sqrt (1-δ^2) * ‖y‖ ≤ ‖project Q P y‖ := by
71   let e := coordinateEquiv P Q δ hδ hsmall hgap hdim
72   let x : P := e.symm y
73   have hxy : project P Q x = y := e.apply_symm_apply y
74   have hxy' : Q.starProjection (x:E) = (y:E) := congrArg Subtype.val hxy
75   have hl := coordinate_lower P Q δ hδ hsmall hgap x
76   rw [hxy] at hl
77   have hi : inner ℝ (P.starProjection (y:E)) (x:E) = ‖y‖^2 := by
78     rw [P.inner_starProjection_left_eq_right, P.starProjection_eq_self_iff.mpr x.property,
79       ← Q.starProjection_eq_self_iff.mpr y.property,
80       Q.inner_starProjection_left_eq_right, hxy']
81     simp
82   have hc := real_inner_le_norm (P.starProjection (y:E)) (x:E)
83   rw [hi] at hc
84   have hp : 0 < Real.sqrt (1-δ^2) := Real.sqrt_pos.mpr (by nlinarith)
85   have hmul := mul_le_mul_of_nonneg_left hc hp.le
86   have hmul' := mul_le_mul_of_nonneg_left hl (norm_nonneg (P.starProjection (y:E)))
87   have hn : ‖project Q P y‖ = ‖P.starProjection (y:E)‖ := rfl
88   rw [hn]
89   by_cases hy : y = 0
90   · simp [hy]
91   · have hypos := norm_pos_iff.mpr hy
92     have hxnorm : ‖(x:E)‖ = ‖x‖ := rfl
93     rw [hxnorm] at hmul
94     nlinarith
95 
96 theorem reverse_residual (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
97     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
98     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) (y : Q) :
99     ‖(y:E)-P.starProjection y‖ ≤ δ*‖y‖ := by
100   have hl := reverse_coordinate_lower P Q δ hδ hsmall hgap hdim y
101   have hn : ‖project Q P y‖ = ‖P.starProjection (y:E)‖ := rfl
102   rw [hn] at hl
103   have hp := P.norm_sq_eq_add_norm_sq_starProjection (y:E)
104   have horth : Pᗮ.starProjection (y:E) = (y:E)-P.starProjection y :=
105     eq_sub_of_add_eq' (P.starProjection_add_starProjection_orthogonal (y:E))
106   rw [horth] at hp
107   have hynorm : ‖(y:E)‖ = ‖y‖ := rfl
108   rw [hynorm] at hp
109   have hs : 0 ≤ 1-δ^2 := by nlinarith
110   have hprod : (Real.sqrt (1-δ^2)*‖y‖)^2 = (1-δ^2)*‖y‖^2 := by
111     rw [mul_pow, Real.sq_sqrt hs]
112   have hsquare : (Real.sqrt (1-δ^2)*‖y‖)^2 ≤ ‖P.starProjection (y:E)‖^2 :=
113     pow_le_pow_left₀ (mul_nonneg (Real.sqrt_nonneg _) (norm_nonneg _)) hl 2
114   nlinarith [norm_nonneg ((y:E)-P.starProjection y), mul_nonneg hδ (norm_nonneg y)]
115 
116 theorem reverse_operator_bound (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
117     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
118     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
119     ‖Q.starProjection.comp Pᗮ.starProjection‖ ≤ δ := by
120   have hr : ‖Pᗮ.starProjection.comp Q.starProjection‖ ≤ δ := by
121     apply ContinuousLinearMap.opNorm_le_bound _ hδ
122     intro v
123     have h := reverse_residual P Q δ hδ hsmall hgap hdim (Q.orthogonalProjectionOnto v)
124     have he : Pᗮ.starProjection (Q.starProjection v) =
125         Q.starProjection v-P.starProjection (Q.starProjection v) :=
126       eq_sub_of_add_eq' (P.starProjection_add_starProjection_orthogonal _)
127     change ‖Pᗮ.starProjection (Q.starProjection v)‖ ≤ δ*‖v‖
128     rw [he]
129     exact h.trans (mul_le_mul_of_nonneg_left (Q.norm_starProjection_apply_le v) hδ)
130   have hn := ContinuousLinearMap.adjoint.norm_map (Pᗮ.starProjection.comp Q.starProjection)
131   rw [ContinuousLinearMap.adjoint_comp,
132     (Q.starProjection_isSymmetric).clm_adjoint_eq,
133     (Pᗮ.starProjection_isSymmetric).clm_adjoint_eq] at hn
134   exact hn.le.trans hr
135 
136 /-- Equal finite dimensions turn a strict one-sided residual into the full gap. -/
137 theorem projection_gap (P Q : Submodule ℝ E) (δ : ℝ) (hδ : 0 ≤ δ)
138     (hsmall : δ < 1) (hgap : ∀ x : P, ‖(x:E)-Q.starProjection x‖ ≤ δ*‖x‖)
139     (hdim : Module.finrank ℝ P = Module.finrank ℝ Q) :
140     ‖P.starProjection-Q.starProjection‖ ≤ δ := by
141   have hr := reverse_operator_bound P Q δ hδ hsmall hgap hdim
142   apply ContinuousLinearMap.opNorm_le_bound _ hδ
143   intro v
144   let a := P.starProjection v
145   let b := Pᗮ.starProjection v
146   have hab : a+b = v := P.starProjection_add_starProjection_orthogonal v
147   have ha : a ∈ P := by simp [a]
148   have hb : Pᗮ.starProjection b = b :=
149     Pᗮ.starProjection_eq_self_iff.mpr (Pᗮ.orthogonalProjectionOnto v).property
150   have hfirst : ‖a-Q.starProjection a‖ ≤ δ*‖a‖ := hgap ⟨a,ha⟩
151   have hsecond : ‖Q.starProjection b‖ ≤ δ*‖b‖ := by
152     have h := (Q.starProjection.comp Pᗮ.starProjection).le_opNorm b
153     change ‖Q.starProjection (Pᗮ.starProjection b)‖ ≤ _ at h
154     rw [hb] at h
155     exact h.trans (mul_le_mul_of_nonneg_right hr (norm_nonneg b))
156   have hi : inner ℝ (a-Q.starProjection a) (Q.starProjection b) = 0 :=
157     Q.starProjection_inner_eq_zero a _ (by simp)
158   have he : (P.starProjection-Q.starProjection) v =
159       (a-Q.starProjection a)-Q.starProjection b := by
160     change a-Q.starProjection v = _
161     rw [← hab, map_add]
162     abel
163   have hp := P.norm_sq_eq_add_norm_sq_starProjection v
164   change ‖v‖^2 = ‖a‖^2+‖b‖^2 at hp
165   have hs1 := pow_le_pow_left₀ (norm_nonneg _) hfirst 2
166   have hs2 := pow_le_pow_left₀ (norm_nonneg _) hsecond 2
167   have hs := norm_sub_sq_real (a-Q.starProjection a) (Q.starProjection b)
168   rw [hi] at hs
169   rw [he]
170   nlinarith [norm_nonneg ((a-Q.starProjection a)-Q.starProjection b),
171     mul_nonneg hδ (norm_nonneg v), mul_pow δ ‖a‖ 2, mul_pow δ ‖b‖ 2,
172     mul_pow δ ‖v‖ 2, mul_nonneg (sq_nonneg δ) (sq_nonneg ‖v‖)]
173 
174 end Komorebi.LSM.OneSidedSubspace

Back to source controls