Schauder Bases and Generalized Bases

This file defines the theory of bases in Banach spaces, unifying the classical sequential notion with modern generalized bases.

Overview

A basis in a normed space allows every vector to be expanded as a (potentially infinite) linear combination of basis vectors. Historically, this was defined strictly for sequences with convergence of partial sums (the "classical Schauder basis").

However, modern functional analysis requires bases indexed by arbitrary sets β (e.g., for non-separable spaces or Hilbert spaces), where convergence is defined via nets over finite subsets (unconditional convergence).

This file provides a unified structure GeneralSchauderBasis that captures both:

• Classical Schauder Bases: Indexed by ℕ, using SummationFilter.conditional to enforce sequential convergence of partial sums.
• Unconditional/Extended Bases: Indexed by an arbitrary type β, using SummationFilter.unconditional to enforce convergence of the net of all finite subsets.

Main Definitions

• GeneralSchauderBasis β 𝕜 X L: A structure representing a generalized Schauder basis for a normed space X over a field 𝕜, indexed by a type β with a SummationFilter L.
• SchauderBasis 𝕜 X: The classical Schauder basis, an abbreviation for GeneralSchauderBasis ℕ 𝕜 X (SummationFilter.conditional ℕ).
• UnconditionalSchauderBasis β 𝕜 X: An unconditional Schauder basis, an abbreviation for GeneralSchauderBasis β 𝕜 X (SummationFilter.unconditional β).
• GeneralSchauderBasis.proj b A: The projection onto a finite set A of basis vectors, mapping x ↦ ∑ i ∈ A, b.coord i x • b i.
• SchauderBasis.proj b n: The n-th projection X → X, mapping x ↦ ∑ i ∈ Finset.range n, b.coord i x • b i.
• UnconditionalSchauderBasis.enormProjBound: The supremum of projection norms (ℝ≥0∞).
• UnconditionalSchauderBasis.nnnormProjBound: The supremum of projection norms (ℝ≥0), requires [CompleteSpace X].
• RankOneDecomposition 𝕜 X: Data for constructing a Schauder basis from a sequence of finite-rank projections whose differences are rank one.
• RankOneDecomposition.basis: Constructs a SchauderBasis from a RankOneDecomposition.

Main Results

• GeneralSchauderBasis.linearIndependent: A Schauder basis is linearly independent.
• GeneralSchauderBasis.tendsto_proj: The projections proj A converge to identity along the summation filter.
• GeneralSchauderBasis.range_proj_eq_span: The range of proj A is the span of the basis elements in A.
• GeneralSchauderBasis.proj_comp: Composition of projections satisfies proj A (proj B x) = proj (A ∩ B) x.
• SchauderBasis.exists_norm_proj_le: In a Banach space, the projections are uniformly bounded.
• UnconditionalSchauderBasis.exists_norm_proj_le: For unconditional bases, projections onto all finite sets are uniformly bounded.

References

• Albiac, Fernando. and Kalton, Nigel J., Topics in Banach Space Theory.
• Singer, Ivan, Bases in Banach spaces.
• Marti, Jürg T., Introduction to the theory of bases.

structure GeneralSchauderBasis (β : Type u_3) (𝕜 : Type u_4) (X : Type u_5) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (L : SummationFilter β) : Type (max (max u_3 u_4) u_5)

A generalized Schauder basis indexed by β with summation along filter L.

The key fields are:

• basis: The basis vectors e i for i : β
• coord: The coordinate functionals f i for i : β in the dual space
• ortho: Biorthogonality condition f i (e j) = if i = j then 1 else 0
• expansion: Every x equals ∑ i, f i x • e i, converging along L

See SchauderBasis for the classical ℕ-indexed case with conditional convergence, and UnconditionalSchauderBasis for the unconditional case.

• basis : β → X

  The basis vectors.

• coord : β → StrongDual 𝕜 X

  Coordinate functionals.

• ortho (i j : β) : (self.coord i) (↑self j) = Pi.single j 1 i

  Biorthogonality.

• expansion (x : X) : HasSum (fun (i : β) => (self.coord i) x • ↑self i) x L

  The sum converges to x along the provided SummationFilter L.

theorem GeneralSchauderBasis.ext {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} {inst✝ : NontriviallyNormedField 𝕜} {inst✝¹ : NormedAddCommGroup X} {inst✝² : NormedSpace 𝕜 X} {L : SummationFilter β} {x y : GeneralSchauderBasis β 𝕜 X L} (basis : ↑x = ↑y) (coord : x.coord = y.coord) : x = y

theorem GeneralSchauderBasis.ext_iff {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} {inst✝ : NontriviallyNormedField 𝕜} {inst✝¹ : NormedAddCommGroup X} {inst✝² : NormedSpace 𝕜 X} {L : SummationFilter β} {x y : GeneralSchauderBasis β 𝕜 X L} : x = y ↔ ↑x = ↑y ∧ x.coord = y.coord

@[reducible, inline]

abbrev SchauderBasis (𝕜 : Type u_4) (X : Type u_5) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Type (max u_4 u_5)

A classical Schauder basis indexed by ℕ with conditional convergence.

Equations

• SchauderBasis 𝕜 X = GeneralSchauderBasis ℕ 𝕜 X (SummationFilter.conditional ℕ)

@[reducible, inline]

abbrev UnconditionalSchauderBasis (β : Type u_4) (𝕜 : Type u_5) (X : Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Type (max (max u_4 u_5) u_6)

An unconditional Schauder basis indexed by β.

In the literature, this is known as:

• An Extended Basis Marti, Jürg T., Introduction to the theory of bases: Defined via convergence of the net of finite partial sums.
• An Unconditional Basis Singer, Ivan., Bases in Banach spaces: On an arbitrary set, convergence is necessarily unconditional.

This structure generalizes the classical Schauder basis by replacing sequential convergence with summability over the directed set of finite subsets.

Equations

• UnconditionalSchauderBasis β 𝕜 X = GeneralSchauderBasis β 𝕜 X (SummationFilter.unconditional β)

@[implicit_reducible]

instance instCoeFunGeneralSchauderBasisForall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} : CoeFun (GeneralSchauderBasis β 𝕜 X L) fun (x : GeneralSchauderBasis β 𝕜 X L) => β → X

Coercion from a GeneralSchauderBasis to the underlying basis function.

Equations

• instCoeFunGeneralSchauderBasisForall = { coe := fun (b : GeneralSchauderBasis β 𝕜 X L) => ↑b }

theorem GeneralSchauderBasis.linearIndependent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) : LinearIndependent 𝕜 ↑b

The basis vectors are linearly independent.

def GeneralSchauderBasis.proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β) : X →L[𝕜] X

Projection onto a finite set of basis vectors.

Equations

• b.proj A = ∑ i ∈ A, ContinuousLinearMap.smulRight (b.coord i) (↑b i)

@[simp]

theorem GeneralSchauderBasis.proj_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) : b.proj ∅ = 0

The projection on the empty set is the zero map.

@[simp]

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

The action of the projection on a vector x.

theorem GeneralSchauderBasis.proj_apply_basis_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β) (i : β) : (b.proj A) (↑b i) = if i ∈ A then ↑b i else 0

The action of the projection on a basis element e i.

theorem GeneralSchauderBasis.tendsto_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (x : X) : Filter.Tendsto (fun (A : Finset β) => (b.proj A) x) L.filter (nhds x)

The projections b.proj A x converge to x along the summation filter.

theorem GeneralSchauderBasis.range_proj_eq_span {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β) : (↑(b.proj A)).range = Submodule.span 𝕜 (↑b '' ↑A)

The range of the projection is the span of the basis elements in A.

theorem GeneralSchauderBasis.proj_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A B : Finset β) (x : X) : (b.proj A) ((b.proj B) x) = (b.proj (A ∩ B)) x

Composition of projections: proj A (proj B x) = proj (A ∩ B) x.

theorem GeneralSchauderBasis.finrank_range_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β) : Module.finrank 𝕜 ↥(↑(b.proj A)).range = A.card

The dimension of the range of the projection proj A equals the cardinality of A.

Unconditional Schauder bases

noncomputable def UnconditionalSchauderBasis.enormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) : ENNReal

The basis constant for unconditional bases (supremum over all finite sets) as enorm.

Equations

• b.enormProjBound = ⨆ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ₑ

theorem UnconditionalSchauderBasis.enorm_proj_le_enormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) (A : Finset β) : ‖GeneralSchauderBasis.proj b A‖ₑ ≤ b.enormProjBound

The enorm of any projection is bounded by the basis constant.

theorem UnconditionalSchauderBasis.exists_norm_proj_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] : ∃ (C : ℝ), ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C

Projections are uniformly bounded for unconditional bases.

noncomputable def UnconditionalSchauderBasis.nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) : NNReal

The basis constant for unconditional bases (supremum over all finite sets) as nnnorm. It requires completeness to guarantee that the supremum is finite, see lemma bddAbove_range_nnnorm_proj below.

Equations

• b.nnnormProjBound = ⨆ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖₊

theorem UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] : BddAbove (Set.range fun (A : Finset β) => ‖GeneralSchauderBasis.proj b A‖₊)

The projection norms are bounded above in a complete space.

theorem UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] (A : Finset β) : ‖GeneralSchauderBasis.proj b A‖₊ ≤ b.nnnormProjBound

The nnnorm of any projection is bounded by the basis constant.

theorem UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] (A : Finset β) : ‖GeneralSchauderBasis.proj b A‖ ≤ ↑b.nnnormProjBound

The norm of any projection is bounded by the basis constant.

ℕ-indexed Schauder bases with conditional convergence

def SchauderBasis.proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ) : X →L[𝕜] X

The n-th projection P_n = b.proj (Finset.range n), given by: P_n x = ∑ i ∈ Finset.range n, b.coord i x • b i

Equations

• b.proj n = GeneralSchauderBasis.proj b (Finset.range n)

@[simp]

theorem SchauderBasis.proj_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) : b.proj 0 = 0

The projection at 0 is the zero map.

@[simp]

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

The action of the projection on a vector.

theorem SchauderBasis.proj_apply_basis_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n i : ℕ) : (b.proj n) (↑b i) = if i < n then ↑b i else 0

The action of the projection on a basis element e i.

theorem SchauderBasis.range_proj_eq_span {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ) : (↑(b.proj n)).range = Submodule.span 𝕜 (↑b '' ↑(Finset.range n))

The range of the projection is the span of the first n basis elements.

theorem SchauderBasis.finrank_range_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ) : Module.finrank 𝕜 ↥(↑(b.proj n)).range = n

The dimension of the range of the projection P n is n.

theorem SchauderBasis.tendsto_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (x : X) : Filter.Tendsto (fun (n : ℕ) => (b.proj n) x) Filter.atTop (nhds x)

The projections converge pointwise to the identity map.

theorem SchauderBasis.proj_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n m : ℕ) (x : X) : (b.proj n) ((b.proj m) x) = (b.proj (min n m)) x

Composition of projections: proj n (proj m x) = proj (min n m) x.

theorem SchauderBasis.exists_norm_proj_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] : ∃ (C : ℝ), ∀ (n : ℕ), ‖b.proj n‖ ≤ C

The projections are uniformly bounded.

noncomputable def SchauderBasis.enormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) : ENNReal

The basis constant for Schauder bases (supremum over projections) as enorm.

Equations

• b.enormProjBound = ⨆ (n : ℕ), ‖b.proj n‖ₑ

theorem SchauderBasis.enorm_proj_le_enormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ) : ‖b.proj n‖ₑ ≤ b.enormProjBound

The enorm of any projection is bounded by the basis constant.

noncomputable def SchauderBasis.nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) : NNReal

The basis constant for Schauder bases (supremum over projections) as nnnorm. Requires completeness to guarantee the supremum is finite, see lemma bddAbove_range_nnnorm_proj below.

Equations

• b.nnnormProjBound = ⨆ (n : ℕ), ‖b.proj n‖₊

theorem SchauderBasis.bddAbove_range_nnnorm_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] : BddAbove (Set.range fun (n : ℕ) => ‖b.proj n‖₊)

The projection norms are bounded above in a complete space.

theorem SchauderBasis.nnnorm_proj_le_nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] (n : ℕ) : ‖b.proj n‖₊ ≤ b.nnnormProjBound

The nnnorm of any projection is bounded by the basis constant.

theorem SchauderBasis.norm_proj_le_nnnormProjBound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] (n : ℕ) : ‖b.proj n‖ ≤ ↑b.nnnormProjBound

The norm of any projection is bounded by the basis constant.

Construction of Schauder basis

We explain how to construct a Schauder basis from a sequence P n of projections satisfying P n ∘ P m = P (min n m), converging to the identity pointwise, and such that each P (n+1) - P n has rank one. The idea is to define the basis vectors as e n = (P (n+1) - P n) x for some x such that this is non-zero, and then show that these vectors form a Schauder basis.

def SchauderBasis.succSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (P : ℕ → X →L[𝕜] X) (n : ℕ) : X →L[𝕜] X

The difference operator P (n + 1) - P n.

Equations

• SchauderBasis.succSub P n = P (n + 1) - P n

@[simp]

theorem SchauderBasis.sum_succSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (P : ℕ → X →L[𝕜] X) (h0 : P 0 = 0) (n : ℕ) : ∑ i ∈ Finset.range n, succSub P i = P n

The sum of succSub operators up to n equals P n.

theorem SchauderBasis.succSub_ortho {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {P : ℕ → X →L[𝕜] X} (hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) (i j : ℕ) (x : X) : (succSub P i) ((succSub P j) x) = if i = j then (succSub P j) x else 0

The operators succSub P i satisfy a biorthogonality relation.

theorem SchauderBasis.finrank_range_succSub_eq_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {P : ℕ → X →L[𝕜] X} (hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n) (hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) (n : ℕ) : Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1

Assuming that the finrank of the range of P n is n then the finrank of the range of succSub P n is 1.

structure SchauderBasis.RankOneDecomposition (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (X : Type u_2) [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Type u_2

Data for constructing a Schauder basis from a sequence of finite-rank projections.

Given a sequence of continuous linear maps P n : X →L[𝕜] X satisfying:

• P 0 = 0 and finrank(range(P n)) = n,
• P n ∘ P m = P (min n m) (the projections are nested and commute),
• P n x → x for every x (pointwise convergence to the identity),

the differences succSub P n = P (n+1) - P n are rank-one operators (see finrank_range_succSub_eq_one). Choosing a nonzero vector e n in the range of each succSub P n yields a Schauder basis for X.

Use RankOneDecomposition.basis to construct the SchauderBasis from this data.

• P : ℕ → X →L[𝕜] X

  The sequence of finite-rank projections.

• e : ℕ → X

  The sequence of candidate basis vectors.

• proj_zero : self.P 0 = 0

  The projections start at 0.

• finrank_range (n : ℕ) : Module.finrank 𝕜 ↥(↑(self.P n)).range = n

  The n-th projection has rank n.

• proj_comp (n m : ℕ) (x : X) : (self.P n) ((self.P m) x) = (self.P (min n m)) x

  The projections commute and are nested P n (P m) = P (min n m).

• proj_tendsto (x : X) : Filter.Tendsto (fun (n : ℕ) => (self.P n) x) Filter.atTop (nhds x)

  The projections converge pointwise to the identity.

• e_mem_range (n : ℕ) : self.e n ∈ (↑(succSub self.P n)).range

  The vector e_n lies in the range of the operator succSub P n = P (n+1) - P n.

• e_ne_zero (n : ℕ) : self.e n ≠ 0

  The vector e_n is non-zero.

theorem SchauderBasis.RankOneDecomposition.exists_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) (n : ℕ) (x : X) : ∃ (c : 𝕜), c • D.e n = (succSub D.P n) x

There exists a coefficient scaling e n to match (succSub D.P n) x.

noncomputable def SchauderBasis.RankOneDecomposition.basisCoeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) (n : ℕ) (x : X) : 𝕜

The coefficient functional value for the basis construction.

Equations

• D.basisCoeff n x = Classical.choose ⋯

@[simp]

theorem SchauderBasis.RankOneDecomposition.basisCoeff_spec {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) (n : ℕ) (x : X) : D.basisCoeff n x • D.e n = (succSub D.P n) x

The coefficient satisfies basisCoeff D n x • D.e n = (succSub D.P n) x.

noncomputable def SchauderBasis.RankOneDecomposition.basis {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) : SchauderBasis 𝕜 X

Constructs a Schauder basis from rank one decomposition.

Equations

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

@[simp]

theorem SchauderBasis.RankOneDecomposition.basis_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) : D.basis.proj = D.P

The projections of the constructed basis correspond to the input data D.P.

@[simp]

theorem SchauderBasis.RankOneDecomposition.basis_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (D : RankOneDecomposition 𝕜 X) : ↑D.basis = D.e

The sequence of the constructed basis corresponds to the input data D.e.