← Verification

ComplementedSubspace/CorollaryStatement.lean

Download original source

Read-only source copy. Line numbers are navigation aids.

1import ComplementedSubspace.TheoremStatement
2import Mathlib.Analysis.Normed.Module.Bases
3import Mathlib.Analysis.Complex.Basic
4
5/-!
6# Exact corollary statements
7
8This file defines the propositions proved by `realCorollary`,
9`realUnconditionalCorollary`, and `realSeparableNonprimarity` in
10`RealMainConsequences.lean`, and by `complexCorollary` in
11`ComplexCorollary.lean`. The scalar multiplier condition uses all scalars of
12norm at most one, including complex phases over the complex field.
13
14Superreflexivity is expressed by its standard equivalent-uniformly-convex-norm
15characterization: bounded linear isomorphism to a complete uniformly convex
16space. We do not substitute algebraic module reflexivity for this property.
17-/
18
19noncomputable section
20universe u
21
22namespace ComplementedSubspace
23
24/-- A Banach-space witness, carrying its actual norm and scalar structure. -/
25structure BanachModel (π•œ : Type*) [NontriviallyNormedField π•œ] where
26 Carrier : Type u
27 normedGroup : NormedAddCommGroup Carrier
28 normedSpace : letI := normedGroup; NormedSpace π•œ Carrier
29 completeSpace : letI := normedGroup; CompleteSpace Carrier
30
31attribute [instance] BanachModel.normedGroup BanachModel.normedSpace BanachModel.completeSpace
32
33variable {π•œ : Type*} [NontriviallyNormedField π•œ]
34 {E : Type u} [NormedAddCommGroup E] [NormedSpace π•œ E]
35
36/-- Existence of a finite or sequential unconditional Schauder basis, matching
37the manuscript's finite-or-natural-number index convention. The finite case
38includes the empty basis of the zero space. Both cases use Mathlib's actual
39biorthogonal continuous coordinates and unconditional convergence. -/
40def HasUnconditionalSchauderBasis (π•œ : Type*) [NontriviallyNormedField π•œ]
41 (E : Type u) [NormedAddCommGroup E] [NormedSpace π•œ E] : Prop :=
42 (βˆƒ n : β„•, Nonempty (UnconditionalSchauderBasis (Fin n) π•œ E)) ∨
43 Nonempty (UnconditionalSchauderBasis β„• π•œ E)
44
45/-- Contractivity for every finitely supported scalar multiplier, not just
46coordinate projections. -/
47def IsOneUnconditional (b : UnconditionalSchauderBasis β„• π•œ E) : Prop :=
48 βˆ€ (s : Finset β„•) (ΞΈ : β„• β†’ π•œ), (βˆ€ i, β€–ΞΈ iβ€– ≀ 1) β†’
49 βˆ€ x : E, β€–βˆ‘ i ∈ s, (ΞΈ i * b.coord i x) β€’ b iβ€– ≀ β€–xβ€–
50
51/-- An actual infinite sequence forming a 1-unconditional Schauder basis.
52This stronger ambient witness is sufficient for the corollaries. Their
53negative range conclusions use `HasUnconditionalSchauderBasis`, which also
54counts finite bases and therefore excludes finite-dimensional loopholes. -/
55def HasOneUnconditionalSchauderBasis (π•œ : Type*) [NontriviallyNormedField π•œ]
56 (E : Type u) [NormedAddCommGroup E] [NormedSpace π•œ E] : Prop :=
57 βˆƒ b : UnconditionalSchauderBasis β„• π•œ E, IsOneUnconditional b
58
59/-- The uniformly convex renormability characterization of superreflexivity. -/
60def IsSuperreflexiveByRenorming (π•œ : Type*) [NontriviallyNormedField π•œ]
61 (E : Type u) [NormedAddCommGroup E] [NormedSpace π•œ E] : Prop :=
62 βˆƒ H : BanachModel.{u} π•œ,
63 UniformConvexSpace H.Carrier ∧ Nonempty (E ≃L[π•œ] H.Carrier)
64
65/-- The quantified target is any real Banach lattice with any equivalent
66norm, not just a lattice order compatible with E's current norm. -/
67def IsIsomorphicToRealBanachLattice (E : Type u) [NormedAddCommGroup E]
68 [NormedSpace ℝ E] : Prop :=
69 βˆƒ L : BanachModel.{u} ℝ,
70 HasRealBanachLatticeOrder L.Carrier ∧ Nonempty (E ≃L[ℝ] L.Carrier)
71
72/-- The unconditional-basis corollary at one scalar field. -/
73def UnconditionalCorollaryStatement (π•œ : Type*) [NontriviallyNormedField π•œ] : Prop :=
74 βˆ€ ρ : ℝ, 0 < ρ β†’ βˆƒ X : BanachModel.{0} π•œ,
75 HasOneUnconditionalSchauderBasis π•œ X.Carrier ∧
76 βˆƒ P : X.Carrier β†’L[π•œ] X.Carrier,
77 P.comp P = P ∧ β€–Pβ€– < 1 + ρ ∧
78 Β¬ HasUnconditionalSchauderBasis π•œ P.range ∧
79 Β¬ HasUnconditionalSchauderBasis π•œ (P.range β†’L[π•œ] π•œ)
80
81/-- The real corollary includes both universal nonlattice conclusions. -/
82def RealCorollaryStatement : Prop :=
83 βˆ€ ρ : ℝ, 0 < ρ β†’ βˆƒ X : BanachModel.{0} ℝ,
84 HasOneUnconditionalSchauderBasis ℝ X.Carrier ∧
85 βˆƒ P : X.Carrier β†’L[ℝ] X.Carrier,
86 P.comp P = P ∧ β€–Pβ€– < 1 + ρ ∧
87 Β¬ HasUnconditionalSchauderBasis ℝ P.range ∧
88 Β¬ HasUnconditionalSchauderBasis ℝ (P.range β†’L[ℝ] ℝ) ∧
89 ¬ IsIsomorphicToRealBanachLattice P.range ∧
90 Β¬ IsIsomorphicToRealBanachLattice (P.range β†’L[ℝ] ℝ)
91
92def ComplexCorollaryStatement : Prop := UnconditionalCorollaryStatement β„‚
93
94/-- Concrete witnesses to the stated separable nonprimarity conclusion. -/
95def SeparableNonprimarityStatement : Prop :=
96 βˆ€ ρ : ℝ, 0 < ρ β†’ βˆƒ X : BanachModel.{0} ℝ,
97 TopologicalSpace.SeparableSpace X.Carrier ∧
98 HasRealBanachLatticeOrder X.Carrier ∧
99 IsSuperreflexiveByRenorming ℝ X.Carrier ∧
100 HasOneUnconditionalSchauderBasis ℝ X.Carrier ∧
101 βˆƒ P : X.Carrier β†’L[ℝ] X.Carrier,
102 P.comp P = P ∧ β€–Pβ€– < 1 + ρ ∧
103 β€–ContinuousLinearMap.id ℝ X.Carrier - Pβ€– < 1 + ρ ∧
104 ¬ IsIsomorphicToRealBanachLattice P.range ∧
105 Β¬ IsIsomorphicToRealBanachLattice
106 (ContinuousLinearMap.id ℝ X.Carrier - P).range
107
108end ComplementedSubspace