Basic facts about generalized Schauder bases

The basis vectors of a generalized Schauder basis span a dense subspace whenever its summation filter is nontrivial, since every vector is a limit of finite coordinate projections.

The coordinate functionals recover the coefficients of a finite sum of basis vectors, and of a basis series converging along any nontrivial summation filter below atTop, not only along the filter of the basis. Precomposing a continuous functional with a finite projection, or with an initial projection of a classical Schauder basis, gives a finite linear combination of coordinate functionals.

An unconditional basis indexed by ℕ is also a classical Schauder basis: convergence along the net of all finite sets implies convergence along initial segments. The conversion UnconditionalSchauderBasis.toSchauderBasis keeps the basis vectors and coordinate functionals, so the classical theory of shrinking and boundedly complete bases applies to unconditional bases such as the coordinate bases of c₀ and ℓᵖ.

The conversion follows Mathlib's HilbertBasis.toSchauderBasis.

theorem GeneralSchauderBasis.dense_span {β : Type u_1} {𝕜 : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) [L.NeBot] : Dense ↑(Submodule.span 𝕜 (Set.range ↑b))

The basis vectors of a generalized Schauder basis span a dense subspace.

@[simp]

theorem GeneralSchauderBasis.coord_sum {β : Type u_1} {𝕜 : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (a : β → 𝕜) {i : β} {s : Finset β} (hi : i ∈ s) : (b.coord i) (∑ j ∈ s, a j • ↑b j) = a i

A coordinate of a finite sum over a set containing i is the prescribed coefficient of i.

theorem GeneralSchauderBasis.comp_proj_eq_sum {β : Type u_1} {𝕜 : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (f : StrongDual 𝕜 X) (A : Finset β) : f ∘SL b.proj A = ∑ i ∈ A, f (↑b i) • b.coord i

Precomposition with a finite projection is a finite linear combination of coordinates.

theorem GeneralSchauderBasis.coord_eq_of_hasSum {β : Type u_1} {𝕜 : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) {L' : SummationFilter β} [L'.NeBot] [L'.LeAtTop] {a : β → 𝕜} {x : X} (h : HasSum (fun (i : β) => a i • ↑b i) x L') (i : β) : (b.coord i) x = a i

Coordinates of a convergent basis series are its coefficients. The series may converge along any nontrivial summation filter L' below atTop, which need not be the filter L of the basis.

theorem SchauderBasis.comp_proj_eq_sum {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (f : StrongDual 𝕜 X) (n : ℕ) : f ∘SL b.proj n = ∑ i ∈ Finset.range n, f (↑b i) • b.coord i

Precomposition with an initial projection is a finite linear combination of coordinates.

def UnconditionalSchauderBasis.toSchauderBasis {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : UnconditionalSchauderBasis ℕ 𝕜 X) : SchauderBasis 𝕜 X

An unconditional basis indexed by ℕ is a classical Schauder basis, with the same basis vectors and coordinate functionals.

@[simp]

theorem UnconditionalSchauderBasis.coe_toSchauderBasis {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : UnconditionalSchauderBasis ℕ 𝕜 X) : ↑b.toSchauderBasis = ↑b

The basis vectors of the classical basis are the original basis vectors.

@[simp]

theorem UnconditionalSchauderBasis.toSchauderBasis_coord {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : UnconditionalSchauderBasis ℕ 𝕜 X) : b.toSchauderBasis.coord = b.coord

The coordinate functionals of the classical basis are the original coordinate functionals.

@[simp]

theorem UnconditionalSchauderBasis.toSchauderBasis_proj {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : UnconditionalSchauderBasis ℕ 𝕜 X) (n : ℕ) : b.toSchauderBasis.proj n = GeneralSchauderBasis.proj b (Finset.range n)

The initial projections of the classical basis are the projections of the unconditional basis onto initial segments.