ComplementedSubspace/LocalUnconditional.lean

1import Mathlib.Analysis.Normed.Operator.NormedSpace

2import Mathlib.Analysis.Normed.Module.Seminorm.Basic

3import Mathlib.LinearAlgebra.StdBasis

4import Mathlib.Topology.Algebra.Module.FiniteDimension

6/-!

7# Real local unconditional structure

9Definitions from `1a-Preliminaries.tex` of the supplied manuscript.

11The unconditional basis constant uses all real coordinate multipliers of

12modulus at most one, not merely coordinate projections. All infima and suprema

13take values in `ℝ≥0∞`; consequently an empty infimum is infinity and no

14attainment of an infimum is asserted. We use the harmless convention `u(0) = 1`

15when defining the unconditional constant of the zero dimensional space.

17For the Gordon--Lewis constant we represent the auxiliary finite dimensional

18space on `Fin n → ℝ`, with an arbitrary positive-definite real seminorm as its

19norm. A factorisation includes certified bounds for its two maps; the infimum

20runs over all these bounds. This is the coordinate version of the manuscript's

21definition with arbitrary finite dimensional Banach spaces and operator norms:

22one transports a chosen 1-unconditional basis to coordinates and pulls back

23the norm. `GLFactorization.ofUnconditionalBasis` implements this direction and

24preserves the exact product of operator norms. Conversely the norm axioms below

25give the actual finite dimensional Banach space `GLFactorization.Aux`.

26`auxBasis_unconditional`, `auxA`, `auxB`, `aux_factorizes`, and

27`aux_cost_le` implement the converse with no increase of the factorisation

28cost. Thus the coordinate presentation has transport maps in both directions;

29no quantification over a proper class of all normed spaces is needed. No main

30theorem is assumed as an axiom.

32The zero subspace is excluded from both outer suprema, exactly as in the

33manuscript. The definitions also make sense for a normed space without a

34completeness hypothesis; applications concern Banach spaces.

35-/

37noncomputable section

39open scoped ENNReal NNReal

41namespace ComplementedSubspace

43section BasisConstants

45variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

47/-- The coordinate multiplier of a finite real basis. Its value on `b i` is

48`θ i • b i`; `constrL` supplies its continuity from finite dimensionality. -/

49def basisMultiplier {n : ℕ} (b : Module.Basis (Fin n) ℝ E)

50 (θ : Fin n → ℝ) : E →L[ℝ] E :=

51 b.constrL (fun i => θ i • b i)

53@[simp]

54theorem basisMultiplier_apply_basis {n : ℕ}

55 (b : Module.Basis (Fin n) ℝ E) (θ : Fin n → ℝ) (i : Fin n) :

56 basisMultiplier b θ (b i) = θ i • b i := by

57 change b.constr ℝ (fun j => θ j • b j) (b i) = _

58 exact b.constr_basis ℝ _ i

60/-- The unconditional constant of a specified finite real basis. The maximum

61with one incorporates the manuscript's convention that constants are ≥ 1. -/

62def unconditionalBasisConstant {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ℝ≥0∞ :=

63 max 1 (⨆ (θ : Fin n → ℝ) (_ : ∀ i, ‖θ i‖ ≤ 1), ‖basisMultiplier b θ‖ₑ)

65theorem one_le_unconditionalBasisConstant {n : ℕ}

66 (b : Module.Basis (Fin n) ℝ E) :

67 1 ≤ unconditionalBasisConstant b :=

68 le_max_left _ _

70/-- The definition controls each admissible multiplier individually. -/

71theorem enorm_basisMultiplier_le {n : ℕ}

72 (b : Module.Basis (Fin n) ℝ E) (θ : Fin n → ℝ)

73 (hθ : ∀ i, ‖θ i‖ ≤ 1) :

74 ‖basisMultiplier b θ‖ₑ ≤ unconditionalBasisConstant b := by

75 apply le_trans _ (le_max_right _ _)

76 exact le_iSup_of_le θ (le_iSup_of_le hθ le_rfl)

78/-- A basis with unconditional constant at most one gives contractions for

79every admissible multiplier. -/

80theorem norm_basisMultiplier_apply_le {n : ℕ}

81 (b : Module.Basis (Fin n) ℝ E)

82 (hb : unconditionalBasisConstant b ≤ 1) (θ : Fin n → ℝ)

83 (hθ : ∀ i, ‖θ i‖ ≤ 1) (x : E) :

84 ‖basisMultiplier b θ x‖ ≤ ‖x‖ := by

85 have he : ‖basisMultiplier b θ‖ₑ ≤ 1 := (enorm_basisMultiplier_le b θ hθ).trans hb

86 have hn : ‖basisMultiplier b θ‖₊ ≤ (1 : ℝ≥0) :=

87 enorm_le_coe.mp (by simpa only [ENNReal.coe_one] using he)

88 have hr : ‖basisMultiplier b θ‖ ≤ (1 : ℝ) := by

89 exact NNReal.coe_le_coe.mpr hn

90 calc

91 ‖basisMultiplier b θ x‖ ≤ ‖basisMultiplier b θ‖ * ‖x‖ :=

92 (basisMultiplier b θ).le_opNorm x

93 _ ≤ 1 * ‖x‖ := mul_le_mul_of_nonneg_right hr (norm_nonneg x)

94 _ = ‖x‖ := one_mul _

96/-- Coordinate reconstruction commutes with the corresponding basis

97multiplier. This is the identity used in transporting auxiliary GL norms. -/

98theorem basisMultiplier_equivFun_symm {n : ℕ}

99 (b : Module.Basis (Fin n) ℝ E) (θ x : Fin n → ℝ) :

100 basisMultiplier b θ (b.equivFun.symm x) =

101 b.equivFun.symm (fun i => θ i * x i) := by

102 change b.constr ℝ (fun i => θ i • b i) (b.equivFun.symm x) = _

103 rw [Module.Basis.constr_apply_fintype, b.equivFun.apply_symm_apply,

104 b.equivFun_symm_apply]

105 simp only [smul_smul, mul_comm]

106

107/-- `u(E)`: infimum of unconditional basis constants over all finite bases.

108It is infinity when no finite basis exists. -/

109def unconditionalConstant (E : Type*) [NormedAddCommGroup E]

110 [NormedSpace ℝ E] : ℝ≥0∞ :=

111 ⨅ (n : ℕ) (b : Module.Basis (Fin n) ℝ E), unconditionalBasisConstant b

112

113theorem one_le_unconditionalConstant (E : Type*) [NormedAddCommGroup E]

114 [NormedSpace ℝ E] : 1 ≤ unconditionalConstant E := by

115 exact le_iInf fun n => le_iInf fun b => one_le_unconditionalBasisConstant b

116

117end BasisConstants

118

119section DPR

120

121variable (Z : Type*) [NormedAddCommGroup Z] [NormedSpace ℝ Z]

122

123/-- Local DPR constant at `V`: infimum of `u(F)` over finite dimensional

124subspaces of the SAME ambient space containing `V`. -/

125def lambdaDPR (V : Submodule ℝ Z) : ℝ≥0∞ :=

126 ⨅ (F : Submodule ℝ Z) (_ : V ≤ F) (_ : FiniteDimensional ℝ ↥F),

127 unconditionalConstant ↥F

128

129/-- Dubinsky--Pełczyński--Rosenthal local unconditional structure constant. -/

130def chiDPR : ℝ≥0∞ :=

131 ⨆ (V : Submodule ℝ Z) (_ : FiniteDimensional ℝ ↥V) (_ : V ≠ ⊥),

132 lambdaDPR Z V

133

134theorem lambdaDPR_le_of_le {V F : Submodule ℝ Z}

135 (hVF : V ≤ F) (hF : FiniteDimensional ℝ ↥F) :

136 lambdaDPR Z V ≤ unconditionalConstant ↥F := by

137 exact iInf_le_of_le F (iInf_le_of_le hVF (iInf_le_of_le hF le_rfl))

138

139theorem one_le_lambdaDPR (V : Submodule ℝ Z) : 1 ≤ lambdaDPR Z V := by

140 exact le_iInf fun F => le_iInf fun _ => le_iInf fun _ =>

141 one_le_unconditionalConstant ↥F

142

143/-- Finiteness, rather than the existence of an optimal witness, defines

144the DPR local unconditional structure property. -/

145def HasDPRLocalUnconditionalStructure : Prop := chiDPR Z < ⊤

146

147end DPR

148

149section GordonLewis

150

151variable {Z : Type*} [NormedAddCommGroup Z] [NormedSpace ℝ Z]

152

153/-- A genuine finite dimensional Gordon--Lewis factorisation, presented on

154coordinates with an arbitrary norm. `b` is NOT required to be injective.

155

156The norm is a positive-definite `Seminorm`, so its triangle inequality,

157homogeneity and nonnegativity are already supplied by mathlib. The coordinate

158basis is 1-unconditional by the displayed contraction condition. -/

159structure GLFactorization (V : Submodule ℝ Z) where

160 dimension : ℕ

161 auxNorm : Seminorm ℝ (Fin dimension → ℝ)

162 positive_definite : ∀ x, auxNorm x = 0 → x = 0

163 unconditional : ∀ (θ x : Fin dimension → ℝ),

164 (∀ i, ‖θ i‖ ≤ 1) → auxNorm (fun i => θ i * x i) ≤ auxNorm x

165 a : ↥V →ₗ[ℝ] (Fin dimension → ℝ)

166 b : (Fin dimension → ℝ) →ₗ[ℝ] Z

167 factorizes : b.comp a = V.subtype

168 aBound : ℝ≥0

169 bBound : ℝ≥0

170 bound_a : ∀ x : ↥V, auxNorm (a x) ≤ (aBound : ℝ) * ‖x‖

171 bound_b : ∀ x : Fin dimension → ℝ, ‖b x‖ ≤ (bBound : ℝ) * auxNorm x

172

173/-- The product of certified operator bounds of a GL factorisation. -/

174def GLFactorization.cost {V : Submodule ℝ Z} (F : GLFactorization V) : ℝ≥0∞ :=

175 (F.aBound : ℝ≥0∞) * (F.bBound : ℝ≥0∞)

176

177@[simp]

178theorem GLFactorization.factorizes_apply {V : Submodule ℝ Z}

179 (F : GLFactorization V) (x : ↥V) : F.b (F.a x) = (x : Z) :=

180 congrArg (fun T : ↥V →ₗ[ℝ] Z => T x) F.factorizes

181

182/-- Injectivity of the first map is a consequence of factorisation, not an

183additional condition on the auxiliary space. -/

184theorem GLFactorization.a_injective {V : Submodule ℝ Z}

185 (F : GLFactorization V) : Function.Injective F.a := by

186 intro x y h

187 apply Subtype.ext

188 calc

189 (x : Z) = F.b (F.a x) := (F.factorizes_apply x).symm

190 _ = F.b (F.a y) := congrArg F.b h

191 _ = (y : Z) := F.factorizes_apply y

192

193/-- The two certified bounds control their composite, which is the inclusion. -/

194theorem GLFactorization.norm_le_bound_mul {V : Submodule ℝ Z}

195 (F : GLFactorization V) (x : ↥V) :

196 ‖x‖ ≤ ((F.bBound : ℝ) * (F.aBound : ℝ)) * ‖x‖ := by

197 calc

198 ‖x‖ = ‖F.b (F.a x)‖ := by rw [F.factorizes_apply]; rfl

199 _ ≤ (F.bBound : ℝ) * F.auxNorm (F.a x) := F.bound_b (F.a x)

200 _ ≤ (F.bBound : ℝ) * ((F.aBound : ℝ) * ‖x‖) :=

201 mul_le_mul_of_nonneg_left (F.bound_a x) F.bBound.2

202 _ = ((F.bBound : ℝ) * (F.aBound : ℝ)) * ‖x‖ := (mul_assoc _ _ _).symm

203

204/-- A factorisation of a nonzero inclusion cannot have cost below one. -/

205theorem GLFactorization.one_le_cost {V : Submodule ℝ Z} [Nontrivial ↥V]

206 (F : GLFactorization V) : 1 ≤ F.cost := by

207 obtain ⟨x, hx⟩ := exists_ne (0 : ↥V)

208 have hreal : (1 : ℝ) ≤ (F.bBound : ℝ) * (F.aBound : ℝ) :=

209 le_of_mul_le_mul_right (by simpa only [one_mul] using F.norm_le_bound_mul x)

210 (norm_pos_iff.mpr hx)

211 have hnn : (1 : ℝ≥0) ≤ F.aBound * F.bBound := by

212 apply NNReal.coe_le_coe.mp

213 simpa only [NNReal.coe_one, NNReal.coe_mul, mul_comm] using hreal

214 simpa only [GLFactorization.cost, ENNReal.coe_one, ENNReal.coe_mul] using

215 (ENNReal.coe_le_coe.mpr hnn)

216

217/-- Transport an actual factorisation through an arbitrary finite dimensional

218normed space with a 1-unconditional basis to the coordinate presentation.

219The stored bounds are EXACTLY the operator norms of its two maps. -/

220def GLFactorization.ofUnconditionalBasis {V : Submodule ℝ Z}

221 {U : Type*} [NormedAddCommGroup U] [NormedSpace ℝ U]

222 {n : ℕ} (e : Module.Basis (Fin n) ℝ U)

223 (he : unconditionalBasisConstant e ≤ 1)

224 (a : ↥V →L[ℝ] U) (b : U →L[ℝ] Z)

225 (h : b.comp a = V.subtypeL) : GLFactorization V where

226 dimension := n

227 auxNorm := (normSeminorm ℝ U).comp e.equivFun.symm.toLinearMap

228 positive_definite := by

229 intro x hx

230 change ‖e.equivFun.symm x‖ = 0 at hx

231 apply e.equivFun.symm.injective

232 simpa only [map_zero] using norm_eq_zero.mp hx

233 unconditional := by

234 intro θ x hθ

235 change ‖e.equivFun.symm (fun i => θ i * x i)‖ ≤ ‖e.equivFun.symm x‖

236 rw [← basisMultiplier_equivFun_symm]

237 exact norm_basisMultiplier_apply_le e he θ hθ _

238 a := e.equivFun.toLinearMap.comp a.toLinearMap

239 b := b.toLinearMap.comp e.equivFun.symm.toLinearMap

240 factorizes := by

241 ext x

242 change b (e.equivFun.symm (e.equivFun (a x))) = (x : Z)

243 rw [e.equivFun.symm_apply_apply]

244 exact congrArg (fun T : ↥V →L[ℝ] Z => T x) h

245 aBound := ‖a‖₊

246 bBound := ‖b‖₊

247 bound_a := by

248 intro x

249 change ‖e.equivFun.symm (e.equivFun (a x))‖ ≤ ‖a‖ * ‖x‖

250 rw [e.equivFun.symm_apply_apply]

251 exact a.le_opNorm x

252 bound_b := by

253 intro x

254 exact b.le_opNorm (e.equivFun.symm x)

255

256@[simp]

257theorem GLFactorization.ofUnconditionalBasis_cost {V : Submodule ℝ Z}

258 {U : Type*} [NormedAddCommGroup U] [NormedSpace ℝ U]

259 {n : ℕ} (e : Module.Basis (Fin n) ℝ U)

260 (he : unconditionalBasisConstant e ≤ 1)

261 (a : ↥V →L[ℝ] U) (b : U →L[ℝ] Z)

262 (h : b.comp a = V.subtypeL) :

263 (GLFactorization.ofUnconditionalBasis e he a b h).cost =

264 (‖a‖₊ : ℝ≥0∞) * (‖b‖₊ : ℝ≥0∞) := rfl

265

266namespace GLFactorization

267

268variable {V : Submodule ℝ Z} (F : GLFactorization V)

269

270/-- A fresh type synonym carries the particular auxiliary norm of `F`, rather

271than the default supremum norm on finite coordinate vectors. -/

272def Aux := Fin F.dimension → ℝ

273

274instance auxAddCommGroup : AddCommGroup F.Aux :=

275 inferInstanceAs (AddCommGroup (Fin F.dimension → ℝ))

276

277instance auxModule : Module ℝ F.Aux :=

278 inferInstanceAs (Module ℝ (Fin F.dimension → ℝ))

279

280/-- Positive definiteness upgrades the stored seminorm to an additive norm. -/

281def auxAddGroupNorm : AddGroupNorm F.Aux where

282 toAddGroupSeminorm := F.auxNorm.toAddGroupSeminorm

283 eq_zero_of_map_eq_zero' := F.positive_definite

284

285instance auxNormedAddCommGroup : NormedAddCommGroup F.Aux :=

286 F.auxAddGroupNorm.toNormedAddCommGroup

287

288instance auxNormedSpace : NormedSpace ℝ F.Aux where

289 norm_smul_le c x := (F.auxNorm.smul' c x).le

290

291instance auxFiniteDimensional : FiniteDimensional ℝ F.Aux :=

292 inferInstanceAs (FiniteDimensional ℝ (Fin F.dimension → ℝ))

293

294instance auxCompleteSpace : CompleteSpace F.Aux :=

295 FiniteDimensional.complete ℝ F.Aux

296

297@[simp]

298theorem aux_norm (x : F.Aux) : ‖x‖ = F.auxNorm x := rfl

299

300/-- The coordinate basis of the actual auxiliary Banach space. -/

301def auxBasis : Module.Basis (Fin F.dimension) ℝ F.Aux :=

302 Pi.basisFun ℝ (Fin F.dimension)

303

304theorem auxBasis_multiplier_apply (θ : Fin F.dimension → ℝ) (x : F.Aux) :

305 basisMultiplier F.auxBasis θ x = fun i => θ i * x i := by

306 have h := basisMultiplier_equivFun_symm F.auxBasis θ x

307 have he : F.auxBasis.equivFun = LinearEquiv.refl ℝ F.Aux :=

308 Pi.basisFun_equivFun ℝ (Fin F.dimension)

309 rw [he] at h

310 exact h

311

312/-- The canonical coordinate basis really has unconditional constant at most

313one in the actual auxiliary normed space. -/

314theorem auxBasis_unconditional : unconditionalBasisConstant F.auxBasis ≤ 1 := by

315 apply max_le le_rfl

316 refine iSup_le fun θ => iSup_le fun hθ => ?_

317 have hn : ‖basisMultiplier F.auxBasis θ‖ ≤ (1 : ℝ) := by

318 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one

319 intro x

320 rw [F.auxBasis_multiplier_apply, one_mul]

321 exact F.unconditional θ x hθ

322 have hn' : ‖basisMultiplier F.auxBasis θ‖₊ ≤ (1 : ℝ≥0) :=

323 NNReal.coe_le_coe.mp hn

324 exact enorm_le_coe.mpr hn'

325

326/-- The first map is continuous for the actual auxiliary norm. -/

327def auxA : ↥V →L[ℝ] F.Aux :=

328 (show ↥V →ₗ[ℝ] F.Aux from F.a).mkContinuous (F.aBound : ℝ) F.bound_a

329

330/-- The second map is continuous for the actual auxiliary norm. -/

331def auxB : F.Aux →L[ℝ] Z :=

332 (show F.Aux →ₗ[ℝ] Z from F.b).mkContinuous (F.bBound : ℝ) F.bound_b

333

334theorem aux_factorizes : F.auxB.comp F.auxA = V.subtypeL := by

335 ext x

336 exact F.factorizes_apply x

337

338theorem norm_auxA_le : ‖F.auxA‖ ≤ (F.aBound : ℝ) :=

339 F.auxA.opNorm_le_bound F.aBound.2 F.bound_a

340

341theorem norm_auxB_le : ‖F.auxB‖ ≤ (F.bBound : ℝ) :=

342 F.auxB.opNorm_le_bound F.bBound.2 F.bound_b

343

344/-- Realizing a coordinate witness as actual bounded operators does not

345increase its cost. Together with `ofUnconditionalBasis_cost` this justifies

346using certified bounds in the infimum. -/

347theorem aux_cost_le :

348 (‖F.auxA‖₊ : ℝ≥0∞) * (‖F.auxB‖₊ : ℝ≥0∞) ≤ F.cost := by

349 have ha : ‖F.auxA‖₊ ≤ F.aBound := NNReal.coe_le_coe.mp F.norm_auxA_le

350 have hb : ‖F.auxB‖₊ ≤ F.bBound := NNReal.coe_le_coe.mp F.norm_auxB_le

351 exact mul_le_mul' (ENNReal.coe_le_coe.mpr ha) (ENNReal.coe_le_coe.mpr hb)

352

353end GLFactorization

354

355variable (Z)

356

357/-- Local Gordon--Lewis constant in the coordinate presentation documented

358above. Every admissible factorisation and every admissible bound is included. -/

359def lambdaGL (V : Submodule ℝ Z) : ℝ≥0∞ :=

360 ⨅ F : GLFactorization V, F.cost

361

362/-- Gordon--Lewis local unconditional structure constant, using arbitrary

363finite dimensional auxiliary norms and excluding the zero initial subspace. -/

364def chiGL : ℝ≥0∞ :=

365 ⨆ (V : Submodule ℝ Z) (_ : FiniteDimensional ℝ ↥V) (_ : V ≠ ⊥),

366 lambdaGL Z V

367

368theorem lambdaGL_le_cost {V : Submodule ℝ Z} (F : GLFactorization V) :

369 lambdaGL Z V ≤ F.cost :=

370 iInf_le _ F

371

372theorem one_le_lambdaGL (V : Submodule ℝ Z) [Nontrivial ↥V] :

373 1 ≤ lambdaGL Z V :=

374 le_iInf fun F => F.one_le_cost

375

376/-- Finiteness of the Gordon--Lewis local unconditional structure constant. -/

377def HasGLLocalUnconditionalStructure : Prop := chiGL Z < ⊤

378

379end GordonLewis

380

381end ComplementedSubspace