Schauder basis of ℓ^p

DefinitionThe unit vectors form an unconditional Schauder basis of ℓᵖ#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(1 \le p < \infty\) and let \(\iota\) be a type. This is the unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\) whose \(i\)-th basis vector is the unit vector \(e_i\), equal to \(1\) at \(i\) and to \(0\) elsewhere, and whose \(i\)-th coordinate functional is the evaluation \(x \mapsto x_i\). In particular every \(x \in \ell^p(\iota, \mathbb{K})\) is the limit in norm of the finite partial sums \(\sum_{i \in A} x_i e_i\) along the finite sets \(A \subseteq \iota\) directed by inclusion.

MathlibExt.Analysis.Normed.Lp.SchauderBasis.lpUnconditionalSchauderBasis · 24 lines

noncomputable def lpUnconditionalSchauderBasis [DecidableEq ι] (hp : p ≠ ⊤) :
    UnconditionalSchauderBasis ι 𝕜 (lp (fun _ : ι => 𝕜) p) where
  basis i := lp.single p i 1
  coord i := lp.evalCLM 𝕜 (fun _ : ι => 𝕜) p i
  ortho i j := by
    have h1 : (lp.evalCLM 𝕜 (fun _ : ι => 𝕜) p i)
        (lp.single (E := fun _ : ι => 𝕜) p j (1 : 𝕜))
        = (lp.single (E := fun _ : ι => 𝕜) p j (1 : 𝕜)) i := rfl
    rw [h1]
    by_cases hij : i = j
    · subst hij
      simp [Pi.single_eq_same]
    · simp [hij, Pi.single_eq_of_ne]
  expansion x := by
    have h : HasSum (fun i : ι => lp.single (E := fun _ : ι => 𝕜) p i (x i)) x :=
      lp.hasSum_single hp x
    have hfun : (fun i : ι => (lp.evalCLM 𝕜 (fun _ : ι => 𝕜) p i) x • lp.single p i (1 : 𝕜))
        = fun i : ι => lp.single (E := fun _ : ι => 𝕜) p i (x i) := by
      funext i
      show (x i) • lp.single (E := fun _ : ι => 𝕜) p i (1 : 𝕜)
        = lp.single (E := fun _ : ι => 𝕜) p i (x i)
      rw [← lp.single_smul, smul_eq_mul, mul_one]
    rw [hfun]
    exact h

Used by 6

Used byBasis vectors of the unconditional ℓᵖ basis · Coordinate functionals of the unconditional ℓᵖ basis · Finite-set projections of the unconditional ℓᵖ basis · The ℓᵖ partial-sum projections are contractions · Basis projections of \(\ell^p\) are contractive · The \(\ell^p\) basis projections have operator norm at most \(1\)

DefinitionThe unit vectors form a Schauder basis of ℓᵖ#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). This is the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) whose \(i\)-th basis vector is the unit vector \(e_i\), equal to \(1\) at \(i\) and to \(0\) elsewhere, and whose \(i\)-th coordinate functional is the evaluation \(x \mapsto x_i\). In particular every \(x \in \ell^p(\mathbb{N}, \mathbb{K})\) is the limit in norm of its partial sums \(\sum_{i < n} x_i e_i\) as \(n \to \infty\).

MathlibExt.Analysis.Normed.Lp.SchauderBasis.lpSchauderBasis · 24 lines

noncomputable def lpSchauderBasis (hp : p ≠ ⊤) :
    SchauderBasis 𝕜 (lp (fun _ : ℕ => 𝕜) p) where
  basis i := lp.single p i 1
  coord i := lp.evalCLM 𝕜 (fun _ : ℕ => 𝕜) p i
  ortho i j := by
    have h1 : (lp.evalCLM 𝕜 (fun _ : ℕ => 𝕜) p i)
        (lp.single (E := fun _ : ℕ => 𝕜) p j (1 : 𝕜))
        = (lp.single (E := fun _ : ℕ => 𝕜) p j (1 : 𝕜)) i := rfl
    rw [h1]
    by_cases hij : i = j
    · subst hij
      simp [Pi.single_eq_same]
    · simp [hij, Pi.single_eq_of_ne]
  expansion x := by
    have h : HasSum (fun i : ℕ => lp.single (E := fun _ : ℕ => 𝕜) p i (x i)) x :=
      lp.hasSum_single hp x
    have hfun : (fun i : ℕ => (lp.evalCLM 𝕜 (fun _ : ℕ => 𝕜) p i) x • lp.single p i (1 : 𝕜))
        = fun i : ℕ => lp.single (E := fun _ : ℕ => 𝕜) p i (x i) := by
      funext i
      show (x i) • lp.single (E := fun _ : ℕ => 𝕜) p i (1 : 𝕜)
        = lp.single (E := fun _ : ℕ => 𝕜) p i (x i)
      rw [← lp.single_smul, smul_eq_mul, mul_one]
    rw [hfun]
    exact h.mono_left SummationFilter.LeAtTop.le_atTop

Used by 9

Used byTruncation equals the Schauder basis projection · Truncation is a contraction on \(\ell^p\) · Truncations of an \(\ell^p\) vector converge to it · Basis vectors of the ℓᵖ Schauder basis · Coordinate functionals of the ℓᵖ Schauder basis · The ℓᵖ partial-sum projections are truncations · The ℓᵖ partial-sum projections are contractions · The ℓᵖ partial-sum projections have norm at most one · Truncations lie in the span of the first basis vectors

TheoremCoordinate functionals of the unconditional ℓᵖ basis#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(1 \le p < \infty\) and let \(\iota\) be a type. For every \(i \in \iota\) and every \(x \in \ell^p(\iota, \mathbb{K})\), the \(i\)-th coordinate functional of the unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\) by unit vectors sends \(x\) to its entry \(x_i\).

@[simp]
theorem lpUnconditionalSchauderBasis_coord_apply [DecidableEq ι] (hp : p ≠ ⊤)
    (i : ι) (x : lp (fun _ : ι => 𝕜) p) :
    (lpUnconditionalSchauderBasis (ι := ι) (𝕜 := 𝕜) (p := p) hp).coord i x = x i

Uses 1 · Used by 1

Statement usesThe unit vectors form an unconditional Schauder basis of ℓᵖ

Used byFinite-set projections of the unconditional ℓᵖ basis

TheoremBasis vectors of the unconditional ℓᵖ basis#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(1 \le p < \infty\) and let \(\iota\) be a type. For every \(i \in \iota\), the \(i\)-th basis vector of the unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\) by unit vectors is the unit vector \(e_i\), the family equal to \(1\) at \(i\) and to \(0\) elsewhere.

@[simp]
theorem lpUnconditionalSchauderBasis_apply [DecidableEq ι] (hp : p ≠ ⊤) (i : ι) :
    (lpUnconditionalSchauderBasis (ι := ι) (𝕜 := 𝕜) (p := p) hp) i
      = lp.single (E := fun _ : ι => 𝕜) p i (1 : 𝕜)

Uses 1 · Used by 1

Statement usesThe unit vectors form an unconditional Schauder basis of ℓᵖ

Used byFinite-set projections of the unconditional ℓᵖ basis

TheoremFinite-set projections of the unconditional ℓᵖ basis#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(1 \le p < \infty\) and let \(\iota\) be a type. For every finite set \(A \subseteq \iota\) and every \(x \in \ell^p(\iota, \mathbb{K})\), the projection \(P_A\) of the unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\) by unit vectors onto the basis vectors indexed by \(A\) satisfies \(P_A x = \sum_{i \in A} x_i e_i\), where \(e_i\) is the unit vector equal to \(1\) at \(i\) and to \(0\) elsewhere.

theorem lpUnconditionalSchauderBasis_proj_apply [DecidableEq ι] (hp : p ≠ ⊤)
    (A : Finset ι) (x : lp (fun _ : ι => 𝕜) p) :
    (lpUnconditionalSchauderBasis (ι := ι) (𝕜 := 𝕜) (p := p) hp).proj A x
      = ∑ i ∈ A, lp.single (E := fun _ : ι => 𝕜) p i (x i)

Uses 3 · Used by 1

Statement usesThe unit vectors form an unconditional Schauder basis of ℓᵖ

Proof usesBasis vectors of the unconditional ℓᵖ basis · Coordinate functionals of the unconditional ℓᵖ basis

Used byBasis projections of \(\ell^p\) are contractive

TheoremBasis projections of \(\ell^p\) are contractive#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be an index set and let \(1 \le p < \infty\). Let \(e_i\) (\(i \in \iota\)) be the unit vectors, which form an unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\). For every finite set \(A \subseteq \iota\) and every \(x \in \ell^p(\iota, \mathbb{K})\), the basis projection \(P_A x = \sum_{i \in A} x_i e_i\) satisfies \(\|P_A x\|_p \le \|x\|_p\).

theorem norm_lpSchauderBasis_proj_apply_le [DecidableEq ι] (hp : p ≠ ⊤)
    (A : Finset ι) (x : lp (fun _ : ι => 𝕜) p) :
    ‖(lpUnconditionalSchauderBasis (ι := ι) (𝕜 := 𝕜) (p := p) hp).proj A x‖ ≤ ‖x‖

Uses 2 · Used by 2

Statement usesThe unit vectors form an unconditional Schauder basis of ℓᵖ

Proof usesFinite-set projections of the unconditional ℓᵖ basis

Used byThe ℓᵖ partial-sum projections are contractions · The \(\ell^p\) basis projections have operator norm at most \(1\)

TheoremThe \(\ell^p\) basis projections have operator norm at most \(1\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be an index set and let \(1 \le p < \infty\). Let \(e_i\) (\(i \in \iota\)) be the unit vectors, which form an unconditional Schauder basis of \(\ell^p(\iota, \mathbb{K})\). For every finite set \(A \subseteq \iota\), the basis projection \(P_A\), the bounded linear operator on \(\ell^p(\iota, \mathbb{K})\) given by \(P_A x = \sum_{i \in A} x_i e_i\), has operator norm \(\|P_A\| \le 1\).

theorem norm_lpSchauderBasis_proj_le [DecidableEq ι] (hp : p ≠ ⊤) (A : Finset ι) :
    ‖(lpUnconditionalSchauderBasis (ι := ι) (𝕜 := 𝕜) (p := p) hp).proj A‖ ≤ 1

Uses 2

Statement usesThe unit vectors form an unconditional Schauder basis of ℓᵖ

Proof usesBasis projections of \(\ell^p\) are contractive

TheoremCoordinate functionals of the ℓᵖ Schauder basis#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). For every \(i \in \mathbb{N}\) and every \(x \in \ell^p(\mathbb{N}, \mathbb{K})\), the \(i\)-th coordinate functional of the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) by unit vectors sends \(x\) to its \(i\)-th entry \(x_i\).

@[simp]
theorem lpSchauderBasis_coord_apply (hp : p ≠ ⊤)
    (i : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    (lpSchauderBasis (𝕜 := 𝕜) (p := p) hp).coord i x = x i

Uses 1 · Used by 1

Statement usesThe unit vectors form a Schauder basis of ℓᵖ

Used byThe ℓᵖ partial-sum projections are truncations

TheoremBasis vectors of the ℓᵖ Schauder basis#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). For every \(i \in \mathbb{N}\), the \(i\)-th basis vector of the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) by unit vectors is the unit vector \(e_i\), the sequence equal to \(1\) at \(i\) and to \(0\) elsewhere.

@[simp]
theorem lpSchauderBasis_apply (hp : p ≠ ⊤) (i : ℕ) :
    (lpSchauderBasis (𝕜 := 𝕜) (p := p) hp) i
      = lp.single (E := fun _ : ℕ => 𝕜) p i (1 : 𝕜)

Uses 1 · Used by 1

Statement usesThe unit vectors form a Schauder basis of ℓᵖ

Used byThe ℓᵖ partial-sum projections are truncations

TheoremThe ℓᵖ partial-sum projections are truncations#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). For every \(n \in \mathbb{N}\) and every \(x \in \ell^p(\mathbb{N}, \mathbb{K})\), the \(n\)-th partial-sum projection \(P_n\) of the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) by unit vectors satisfies \(P_n x = \sum_{i < n} x_i e_i\), where \(e_i\) is the unit vector equal to \(1\) at \(i\) and to \(0\) elsewhere; that is, \(P_n x\) is the truncation of \(x\) to its first \(n\) coordinates.

theorem lpSchauderBasis_proj_apply (hp : p ≠ ⊤)
    (n : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    (lpSchauderBasis (𝕜 := 𝕜) (p := p) hp).proj n x
      = ∑ i ∈ Finset.range n, lp.single (E := fun _ : ℕ => 𝕜) p i (x i)

Uses 3 · Used by 1

Statement usesThe unit vectors form a Schauder basis of ℓᵖ

Proof usesBasis vectors of the ℓᵖ Schauder basis · Coordinate functionals of the ℓᵖ Schauder basis

Used byTruncation equals the Schauder basis projection

TheoremThe ℓᵖ partial-sum projections are contractions#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). For every \(n \in \mathbb{N}\) and every \(x \in \ell^p(\mathbb{N}, \mathbb{K})\), the \(n\)-th partial-sum projection \(P_n\) of the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) by unit vectors satisfies \(\|P_n x\| \le \|x\|\).

theorem norm_lpSchauderBasis_classical_proj_apply_le (hp : p ≠ ⊤)
    (n : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    ‖(lpSchauderBasis (𝕜 := 𝕜) (p := p) hp).proj n x‖ ≤ ‖x‖

Uses 3 · Used by 2

Statement usesThe unit vectors form a Schauder basis of ℓᵖ

Proof usesThe unit vectors form an unconditional Schauder basis of ℓᵖ · Basis projections of \(\ell^p\) are contractive

Used byTruncation is a contraction on \(\ell^p\) · The ℓᵖ partial-sum projections have norm at most one

TheoremThe ℓᵖ partial-sum projections have norm at most one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le p < \infty\). For every \(n \in \mathbb{N}\), the \(n\)-th partial-sum projection of the Schauder basis of \(\ell^p(\mathbb{N}, \mathbb{K})\) by unit vectors has operator norm at most \(1\).

theorem norm_lpSchauderBasis_classical_proj_le (hp : p ≠ ⊤) (n : ℕ) :
    ‖(lpSchauderBasis (𝕜 := 𝕜) (p := p) hp).proj n‖ ≤ 1

Uses 2

Statement usesThe unit vectors form a Schauder basis of ℓᵖ

Proof usesThe ℓᵖ partial-sum projections are contractions

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.