Unconditional Schauder Bases

Source: doi:10.1007/978-3-662-53294-2 Authors: Daniel Smania Status: verified Main declarations: UnconditionalCriterion.exists_unconditionalSchauderBasis_of_finiteSignBound Tags: functional-analysis, banach-spaces, schauder-bases MSC: 46B15

Schauder bases and the finite sign criterion

This file develops a small API for Schauder bases and proves a finite sign criterion for constructing unconditional Schauder bases.

The main ingredients are:

• SchauderBasis and UnconditionalSchauderBasis, the usual ℕ-indexed notions. A Schauder expansion is ordered, so its convergence is expressed by initial partial sums.
• Rearrangement criteria for SchauderBasis.IsUnconditional, including HasSum reindexing, convergence over the finite-set filter, and the classical ordered partial-sum criterion for every permutation of ℕ.
• UnconditionalSchauderBasisAbstractIndex is indexed by an arbitrary type. Its expansion uses HasSum, which is the unconditional finite-set filter.
• UnconditionalCriterion.exists_unconditionalSchauderBasisAbstractIndex_of_finiteSignBound and UnconditionalCriterion.exists_unconditionalSchauderBasis_of_finiteSignBound, which package the construction of an unconditional Schauder basis from a uniform finite sign estimate, dense span, and nonzero vectors.

The finite sign criterion is first proved for an arbitrary index type. The usual ℕ-indexed theorem is then recovered by enumeration with Equiv.refl ℕ.

ℕ-indexed Schauder bases

The ordered notion of a Schauder sum is separated out because it is weaker than HasSum: a Schauder basis need only converge along the initial segments Finset.range N.

def HasSchauderSum {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (basis : ℕ → E) (a : ℕ → 𝕜) (x : E) : Prop

The ordered partial-sum convergence used by Schauder bases.

HasSchauderSum basis a x means that ∑ n ∈ Finset.range N, a n • basis n tends to x as N → ∞.

Equations

• HasSchauderSum basis a x = Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, a n • basis n) Filter.atTop (nhds x)

structure SchauderBasis (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : Type (max u_1 u_2)

A Schauder basis for a complete normed space.

For each vector x, the initial partial sums of the coordinate expansion converge to x, and this expansion is unique. The coordinate maps are stored as continuous linear maps.

• basis : ℕ → E

  Basis vectors.

• coeff : ℕ → E →L[𝕜] 𝕜

  Continuous coordinate maps.

• hasSchauderSum_repr (x : E) : HasSchauderSum self.basis (fun (n : ℕ) => (self.coeff n) x) x

  Every vector equals the limit of the initial partial sums of its expansion.

• unique_coeff (x : E) (a : ℕ → 𝕜) : HasSchauderSum self.basis a x → a = fun (n : ℕ) => (self.coeff n) x

  Coefficients in this expansion are unique.

def SchauderBasis.coord {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) (n : ℕ) (x : E) : 𝕜

The nth coordinate of x in the basis b.

Equations

• b.coord n x = (b.coeff n) x

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

A Schauder basis is unconditional if every basis expansion has a HasSum.

Since HasSum is Lean's unconditional finite-set notion of summability, this immediately implies ordered convergence of every permuted expansion; see SchauderBasis.isUnconditional_tendsto_rearranged.

Equations

• b.IsUnconditional = ∀ (x : E), HasSum (fun (n : ℕ) => (b.coeff n) x • b.basis n) x

theorem SchauderBasis.isUnconditional_iff_hasSum_rearranged {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) : b.IsUnconditional ↔ ∀ (x : E) (σ : Equiv.Perm ℕ), HasSum (fun (n : ℕ) => (b.coeff (σ n)) x • b.basis (σ n)) x

HasSum unconditionality is invariant under every permutation of ℕ.

This is a useful technical form of unconditionality, but it is still phrased in terms of HasSum, so it is mostly a reindexing statement. For the ordered partial-sum formulation, see SchauderBasis.isUnconditional_tendsto_rearranged.

theorem SchauderBasis.isUnconditional_iff_tendsto_rearranged {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) : b.IsUnconditional ↔ ∀ (x : E) (σ : Equiv.Perm ℕ), Filter.Tendsto (fun (s : Finset ℕ) => ∑ n ∈ s, (b.coeff (σ n)) x • b.basis (σ n)) Filter.atTop (nhds x)

Unconditionality is equivalent to strong convergence of all rearranged finite partial-sum nets.

This is the same mathematical content as SchauderBasis.isUnconditional_iff_hasSum_rearranged, but it exposes the underlying Filter.Tendsto statement instead of the abbreviation HasSum. The filter is atTop on Finset ℕ, so finite sets eventually contain any prescribed finite set of indices.

theorem SchauderBasis.isUnconditional_tendsto_rearranged {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) : b.IsUnconditional → ∀ (x : E) (σ : Equiv.Perm ℕ), Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, (b.coeff (σ n)) x • b.basis (σ n)) Filter.atTop (nhds x)

Unconditionality implies convergence of every permuted ordered expansion.

For every vector x and permutation σ, the initial partial sums ∑ n ∈ Finset.range N, coeff (σ n) x • basis (σ n) tend to x in the norm topology. This is the direct Lean version of the usual statement that every rearrangement of the Schauder expansion converges to the same vector.

theorem SchauderBasis.isUnconditional_iff_tendsto_ordered_rearranged {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) : b.IsUnconditional ↔ ∀ (x : E) (σ : Equiv.Perm ℕ), Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, (b.coeff (σ n)) x • b.basis (σ n)) Filter.atTop (nhds x)

Unconditionality is equivalent to ordered convergence of every rearranged expansion.

This is the classical rearrangement formulation: for every vector x and every permutation σ : Equiv.Perm ℕ, the initial partial sums over Finset.range N of the permuted expansion converge to x.

structure UnconditionalSchauderBasis (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : Type (max u_1 u_2)

An unconditional Schauder basis with the usual ℕ index set.

This is a Schauder basis together with unconditional summability of every basis expansion. The classical ordered rearrangement criterion is available as SchauderBasis.isUnconditional_iff_tendsto_ordered_rearranged.

• toSchauderBasis : SchauderBasis 𝕜 E

  Underlying Schauder basis.

• unconditional : self.toSchauderBasis.IsUnconditional

  Every basis expansion converges unconditionally to the same sum.

Abstractly indexed unconditional bases

For an arbitrary index type there is no preferred order of partial sums. The natural primitive statement is therefore unconditional summability over finite subsets, i.e. HasSum.

structure UnconditionalSchauderBasisAbstractIndex (𝕜 : Type u_1) (Index : Type u_2) (E : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : Type (max (max u_1 u_2) u_3)

An unconditional Schauder basis indexed by an arbitrary type.

Here basis i is the vector φᵢ, coeff i is the corresponding coordinate functional, and every vector has a unique unconditional expansion over the whole index type. This abstract version is the natural target for the finite sign criterion, where no preferred order on the index set is needed.

• basis : Index → E

  Basis vectors, indexed by an arbitrary type.

• coeff : Index → E →L[𝕜] 𝕜

  Continuous coordinate functionals, with the same index type.

• hasSum_repr (x : E) : HasSum (fun (i : Index) => (self.coeff i) x • self.basis i) x

  Every vector is the unconditional sum of its abstractly indexed expansion.

• unique_coeff (x : E) (a : Index → 𝕜) : HasSum (fun (i : Index) => a i • self.basis i) x → a = fun (i : Index) => (self.coeff i) x

  Coefficients in such an unconditional expansion are unique.

@[simp]

theorem UnconditionalSchauderBasisAbstractIndex.hasSum_repr_apply {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (x : E) : HasSum (fun (i : Index) => (b.coeff i) x • b.basis i) x

The representation theorem of an abstract unconditional Schauder basis, as a simp lemma.

theorem UnconditionalSchauderBasisAbstractIndex.unique_coeff_apply {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (x : E) (a : Index → 𝕜) (ha : HasSum (fun (i : Index) => a i • b.basis i) x) : a = fun (i : Index) => (b.coeff i) x

Coefficients in an abstract unconditional expansion are the stored coordinate maps.

Coordinates of basis vectors

The next two lemmas extract the usual Kronecker-delta behaviour of the coordinate maps from uniqueness of unconditional expansions.

theorem UnconditionalSchauderBasisAbstractIndex.coeff_basis_self {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (i : Index) : (b.coeff i) (b.basis i) = 1

The coordinate maps take value 1 on their own basis vector.

theorem UnconditionalSchauderBasisAbstractIndex.coeff_basis_ne {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) {i j : Index} (hji : j ≠ i) : (b.coeff i) (b.basis j) = 0

The coordinate maps vanish on the other basis vectors.

Enumerating an abstract basis

If an abstract index type is equivalent to ℕ, then any enumeration gives an ordinary unconditional Schauder basis. The construction uses HasSum to get the ordered Schauder convergence, and the Kronecker-delta lemmas above to prove uniqueness of ordered coefficients.

noncomputable def UnconditionalSchauderBasisAbstractIndex.toUnconditionalSchauderBasis {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (e : ℕ ≃ Index) : UnconditionalSchauderBasis 𝕜 E

Enumerating an abstract unconditional Schauder basis gives a usual ℕ-indexed unconditional Schauder basis.

The equivalence e : ℕ ≃ Index provides the order used for the Schauder partial sums. Unconditional summability supplies convergence for that order, while uniqueness of abstract coordinates gives uniqueness of the ordered coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem UnconditionalSchauderBasisAbstractIndex.range_basis_toUnconditionalSchauderBasis {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (e : ℕ ≃ Index) : Set.range (b.toUnconditionalSchauderBasis e).toSchauderBasis.basis = Set.range b.basis

Enumerating an abstract basis does not change the set of basis vectors.

theorem UnconditionalSchauderBasisAbstractIndex.range_coeff_toUnconditionalSchauderBasis {𝕜 : Type u_1} {Index : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E) (e : ℕ ≃ Index) : Set.range (b.toUnconditionalSchauderBasis e).toSchauderBasis.coeff = Set.range b.coeff

Enumerating an abstract basis does not change the set of coordinate maps.

Basic API for unconditional Schauder bases

This namespace provides convenient projections to the underlying basis and coordinate maps, plus the reverse conversion from the usual ℕ-indexed notion to the abstract-index notion with Index = ℕ.

@[implicit_reducible]

instance UnconditionalSchauderBasis.instCoeSchauderBasis {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : Coe (UnconditionalSchauderBasis 𝕜 E) (SchauderBasis 𝕜 E)

Equations

• UnconditionalSchauderBasis.instCoeSchauderBasis = { coe := fun (b : UnconditionalSchauderBasis 𝕜 E) => b.toSchauderBasis }

def UnconditionalSchauderBasis.basis {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasis 𝕜 E) : ℕ → E

Basis vectors of an unconditional Schauder basis.

Equations

• b.basis = b.toSchauderBasis.basis

def UnconditionalSchauderBasis.coeff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasis 𝕜 E) : ℕ → E →L[𝕜] 𝕜

Continuous coordinate maps of an unconditional Schauder basis.

Equations

• b.coeff = b.toSchauderBasis.coeff

def UnconditionalSchauderBasis.toUnconditionalSchauderBasisAbstractIndex {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasis 𝕜 E) : UnconditionalSchauderBasisAbstractIndex 𝕜 ℕ E

Forget the order on an unconditional Schauder basis and regard it as an abstractly indexed basis over ℕ.

The HasSum part of unconditionality becomes the representation theorem for the abstract basis, while uniqueness is inherited from the ordered Schauder basis by passing a HasSum to its ordered partial sums.

Equations

• b.toUnconditionalSchauderBasisAbstractIndex = { basis := b.basis, coeff := b.coeff, hasSum_repr := ⋯, unique_coeff := ⋯ }

theorem UnconditionalSchauderBasis.exists_unconditionalSchauderBasisAbstractIndex_nat {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (b : UnconditionalSchauderBasis 𝕜 E) : ∃ (b' : UnconditionalSchauderBasisAbstractIndex 𝕜 ℕ E), b'.basis = b.basis ∧ b'.coeff = b.coeff

Every unconditional Schauder basis gives an abstractly indexed one over ℕ with the same basis vectors and coordinate maps.

Finite sign criterion

This section proves a practical criterion for building unconditional Schauder bases from finite estimates.

The core theorem is indexed by an arbitrary type Index. The hypotheses are:

• x : Index → E has dense closed linear span,
• no vector x i is zero,
• and if finite signed sums satisfy ‖∑ i ∈ s, (ε i * a i) • x i‖ ≤ C * ‖∑ i ∈ s, a i • x i‖,

then x determines an UnconditionalSchauderBasisAbstractIndex.

The usual ℕ-indexed theorem is recovered at the end by specializing Index = ℕ and enumerating with Equiv.refl ℕ.

def UnconditionalCriterion.HasDenseSpan {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {Index : Type u_3} (x : Index → E) : Prop

The closed linear span of x is all of E.

In infinite-dimensional Banach spaces, this is the right meaning of "the vectors x i span E".

Equations

• UnconditionalCriterion.HasDenseSpan x = (closure ↑(Submodule.span 𝕜 (Set.range x)) = Set.univ)

def UnconditionalCriterion.HasFiniteSignBound {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {Index : Type u_3} (x : Index → E) (C : ℝ) : Prop

Finite sign estimate for the family x.

This says that changing finitely many coefficients by signs can increase the norm of the corresponding finite sum by at most the factor C:

‖∑_{i ∈ s} ε_i a_i x_i‖ ≤ C ‖∑_{i ∈ s} a_i x_i‖,

with each ε_i equal to 1 or -1 on the finite set s.

Equations

• UnconditionalCriterion.HasFiniteSignBound x C = ∀ (s : Finset Index) (a ε : Index → 𝕜), (∀ i ∈ s, ε i = 1 ∨ ε i = -1) → ‖∑ i ∈ s, (ε i * a i) • x i‖ ≤ C * ‖∑ i ∈ s, a i • x i‖

From signs to projection bounds

The sign estimate is first converted into a uniform bound for finite coordinate projections. This is the finite-dimensional algebraic part of the argument.

Algebraic coordinates on the span

The projection bound implies linear independence and bounds the coordinate functionals on the algebraic span. Density then lets us extend those functionals continuously to all of E.

Convergence and uniqueness of the constructed expansion

The analytic core proves that the finite coordinate projections converge to the identity along the finite-set filter. This gives the HasSum representation. Uniqueness follows by applying coordinate functionals to any other unconditional expansion.

Packaging the basis

The private constructor packages the coordinate maps and the two analytic facts into UnconditionalSchauderBasisAbstractIndex. The public theorems below expose only existence and keep the construction details hidden.

theorem UnconditionalCriterion.exists_unconditionalSchauderBasisAbstractIndex_of_finiteSignBound {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {Index : Type u_3} (x : Index → E) (hx_dense : HasDenseSpan x) (hx_ne : ∀ (i : Index), x i ≠ 0) (C : ℝ) (hC : 0 ≤ C) (h_sign : HasFiniteSignBound x C) : ∃ (b : UnconditionalSchauderBasisAbstractIndex 𝕜 Index E), b.basis = x

Abstract-index finite sign criterion.

If x has dense closed linear span, no vector x i is zero, and finite sign changes are uniformly bounded by C, then there is an abstractly indexed unconditional Schauder basis whose basis family is exactly x.

theorem UnconditionalCriterion.exists_unconditionalSchauderBasis_of_finiteSignBound {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (x : ℕ → E) (hx_dense : HasDenseSpan x) (hx_ne : ∀ (i : ℕ), x i ≠ 0) (C : ℝ) (hC : 0 ≤ C) (h_sign : HasFiniteSignBound x C) : ∃ (b : UnconditionalSchauderBasis 𝕜 E), b.basis = x

Main finite sign criterion for sequences.

If x : ℕ → E has dense closed linear span, no vector x n is zero, and finite sign changes are uniformly bounded by C, then x is the basis sequence of an unconditional Schauder basis.

This theorem is kept for the usual ℕ-indexed API; internally it is just the abstract-index criterion specialized to ℕ.