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 Banach space.

For each vector x, the series ∑' n, coeff n x • basis n converges 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.

• hasSum_repr (x : E) : HasSum (fun (n : ℕ) => (self.coeff n) x • self.basis n) x

  Every vector equals the sum of its basis expansion.

• unique_coeff (x : E) (a : ℕ → 𝕜) : HasSum (fun (n : ℕ) => a n • self.basis n) 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 permuting the terms of the basis series does not change its sum.

Equations

• b.IsUnconditional = ∀ (x : E) (σ : Equiv.Perm ℕ), HasSum (fun (n : ℕ) => (b.coeff (σ n)) x • b.basis (σ n)) 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.

This is a Schauder basis together with the statement that every rearranged basis expansion still converges to the same vector.

• toSchauderBasis : SchauderBasis 𝕜 E

  Underlying Schauder basis.

• unconditional : self.toSchauderBasis.IsUnconditional

  Every rearranged basis expansion converges to the same sum.

@[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

From a finite sign estimate to an unconditional Schauder basis

This section proves a practical criterion for building an unconditional Schauder basis.

We work in Banach spaces over a nontrivially normed field of characteristic zero, with sequences indexed by ℕ.

Mathematically, the theorem is:

• if x : ℕ → E has dense closed linear span,
• if no x n 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 unconditional Schauder basis.

We separate finite-dimensional algebra from analytic arguments so each step is easier to follow.

def UnconditionalCriterion.HasDenseSpan {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : ℕ → 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 n 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] (x : ℕ → E) (C : ℝ) : Prop

Finite sign estimate.

This is

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

with each ε_i equal to 1 or -1.

Equations

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

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 : ∀ (n : ℕ), x n ≠ 0) (C : ℝ) (hC : 0 ≤ C) (h_sign : HasFiniteSignBound x C) : ∃ (b : UnconditionalSchauderBasis 𝕜 E), b.basis = x

Main existence theorem: finite sign bound + dense span + x n ≠ 0 produce an unconditional Schauder basis whose basis sequence is exactly x.