Theorems · Inductive type · functional analysis

GeneralSchauderBasis

(β : Type u_3) →
  (𝕜 : Type u_4) →
    (X : Type u_5) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → 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.

Defined in

Mathlib.Analysis.Normed.Module.Bases

Cited by

16 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace