Schauder bases and reflexivity

A Schauder basis is shrinking if its coordinate functionals span a norm-dense subspace of the continuous dual. It is boundedly complete if every scalar sequence with bounded initial partial sums gives a convergent basis expansion.

James's basis criterion characterizes reflexivity by these two properties. All series here use initial segments, rather than unconditional summation.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §4.4, Theorem 4.4.15.

def SchauderBasis.IsShrinking {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) : Prop

A basis is shrinking when its coordinate functionals span a norm-dense subspace of the continuous dual.

theorem SchauderBasis.isShrinking_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) : b.IsShrinking ↔ (Submodule.span 𝕜 (Set.range b.coord)).topologicalClosure = ⊤

A basis is shrinking precisely when the norm closure of the span of its coordinate functionals is the whole continuous dual.

def SchauderBasis.IsBoundedlyComplete {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) : Prop

A basis is boundedly complete when bounded initial partial sums of any scalar sequence converge in norm. The summation filter is the conditional one.

theorem SchauderBasis.isBoundedlyComplete_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) : b.IsBoundedlyComplete ↔ ∀ (a : ℕ → 𝕜), BddAbove (Set.range fun (n : ℕ) => ‖∑ i ∈ Finset.range n, a i • ↑b i‖) → ∃ (x : E), ∀ (i : ℕ), (b.coord i) x = a i

Bounded completeness says precisely that every coefficient sequence with bounded initial partial sums is the coordinate sequence of a vector.

theorem SchauderBasis.IsShrinking.ext {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {b : SchauderBasis 𝕜 E} (hb : b.IsShrinking) {Φ Ψ : StrongDual 𝕜 (StrongDual 𝕜 E)} (h : ∀ (i : ℕ), Φ (b.coord i) = Ψ (b.coord i)) : Φ = Ψ

A shrinking basis determines continuous bidual functionals by their values on the coordinate functionals.

theorem SchauderBasis.isShrinking_of_surjective_inclusionInDoubleDual {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) (hE : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)) : b.IsShrinking

Every Schauder basis of a reflexive space is shrinking. Completeness follows from reflexivity and need not be assumed separately.

theorem SchauderBasis.isBoundedlyComplete_of_surjective_inclusionInDoubleDual {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) (hE : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)) : b.IsBoundedlyComplete

Every Schauder basis of a reflexive space is boundedly complete.

theorem SchauderBasis.surjective_inclusionInDoubleDual_of_isShrinking_of_isBoundedlyComplete {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) [CompleteSpace E] (hs : b.IsShrinking) (hc : b.IsBoundedlyComplete) : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)

A shrinking and boundedly complete Schauder basis makes its space reflexive.

theorem SchauderBasis.surjective_inclusionInDoubleDual_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) [CompleteSpace E] : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E) ↔ b.IsShrinking ∧ b.IsBoundedlyComplete

James's basis criterion. A Banach space with a Schauder basis is reflexive if and only if that basis is shrinking and boundedly complete.