Duals of ℓ^p and c₀

DefinitionCanonical duality pairing between \(\ell^q\) and \(\ell^p\)#✓fully proved

The canonical pairing ℓ^q × ℓ^p → 𝕜, as a continuous linear map ℓ^q →L[𝕜] (ℓ^p →L[𝕜] 𝕜).

noncomputable def lpDualPairing :
    lp (fun _ : ι => 𝕜) q →L[𝕜] StrongDual 𝕜 (lp (fun _ : ι => 𝕜) p) := by
  exact lp.dualPairing (K := 1) q p (fun _ => ContinuousLinearMap.mul 𝕜 𝕜)
    (fun _ => by rw [NNReal.coe_one]; exact ContinuousLinearMap.opNorm_mul_le 𝕜 𝕜)

Used by 5

Used byDual of \(\ell^p\) is isometric to \(\ell^q\) · Duality pairing as a sum of coordinatewise products · Duality pairing is norm-preserving · Every functional on \(\ell^p\) comes from an \(\ell^q\) sequence · Duality pairing has operator norm at most one

TheoremDuality pairing as a sum of coordinatewise products#✓fully proved

The pairing is given by the sum of coordinatewise products.

theorem lpDualPairing_apply (a : lp (fun _ : ι => 𝕜) q)
    (x : lp (fun _ : ι => 𝕜) p) :
    lpDualPairing (𝕜 := 𝕜) (ι := ι) (p := p) (q := q) a x = ∑' i, a i * x i

Uses 1 · Used by 2

Statement usesCanonical duality pairing between \(\ell^q\) and \(\ell^p\)

Used byDuality pairing is norm-preserving · Every functional on \(\ell^p\) comes from an \(\ell^q\) sequence

TheoremDuality pairing has operator norm at most one#✓fully proved

The pairing has operator norm at most one.

theorem norm_lpDualPairing_le :
    ‖lpDualPairing (𝕜 := 𝕜) (ι := ι) (p := p) (q := q)‖ ≤ 1

Uses 1 · Used by 1

Statement usesCanonical duality pairing between \(\ell^q\) and \(\ell^p\)

Used byDuality pairing is norm-preserving

TheoremEvery functional on \(\ell^p\) comes from an \(\ell^q\) sequence#✓fully proved

The pairing is surjective: every continuous linear functional on ℓ^p is given by pairing with some ℓ^q sequence.

theorem lpDualPairing_surjective (hp_top : p ≠ ⊤) :
    Function.Surjective (lpDualPairing (𝕜 := 𝕜) (ι := ι) (p := p) (q := q))

Uses 2 · Used by 1

Statement usesCanonical duality pairing between \(\ell^q\) and \(\ell^p\)

Proof usesDuality pairing as a sum of coordinatewise products

Used byDual of \(\ell^p\) is isometric to \(\ell^q\)

TheoremDuality pairing is norm-preserving#✓fully proved

The pairing is norm-preserving.

theorem lpDualPairing_norm (hp_top : p ≠ ⊤) (a : lp (fun _ : ι => 𝕜) q) :
    ‖lpDualPairing (𝕜 := 𝕜) (ι := ι) (p := p) (q := q) a‖ = ‖a‖

Uses 3 · Used by 1

Statement usesCanonical duality pairing between \(\ell^q\) and \(\ell^p\)

Proof usesDuality pairing as a sum of coordinatewise products · Duality pairing has operator norm at most one

Used byDual of \(\ell^p\) is isometric to \(\ell^q\)

DefinitionDual of \(\ell^p\) is isometric to \(\ell^q\)#✓fully proved

The dual of ℓ^p is isometrically isomorphic to ℓ^q.

noncomputable def lpDualEquiv (hp_top : p ≠ ⊤) :
    lp (fun _ : ι => 𝕜) q ≃ₗᵢ[𝕜] StrongDual 𝕜 (lp (fun _ : ι => 𝕜) p) := by
  classical
  exact LinearIsometryEquiv.ofSurjective
    ⟨(lpDualPairing (𝕜 := 𝕜) (ι := ι) (p := p) (q := q)).toLinearMap,
      fun a => lpDualPairing_norm hp_top a⟩
    (lpDualPairing_surjective hp_top)

Uses 3

Statement usesCanonical duality pairing between \(\ell^q\) and \(\ell^p\) · Duality pairing is norm-preserving · Every functional on \(\ell^p\) comes from an \(\ell^q\) sequence

DefinitionThe subspace of null sequences in \(\ell^\infty\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. The sequences \(x \in \ell^\infty(\iota, \mathbb{K})\) whose coordinates \(x_i\) tend to \(0\) along the cofinite filter on \(\iota\) form a \(\mathbb{K}\)-linear subspace of \(\ell^\infty(\iota, \mathbb{K})\).

MathlibExt.Analysis.Normed.Lp.DualC0.c0Submodule · 22 lines

noncomputable def c0Submodule (𝕜 : Type u) [RCLike 𝕜] (ι : Type v) :
    Submodule 𝕜 (lp (fun _ : ι => 𝕜) ∞) where
  carrier := { f | Filter.Tendsto (⇑f) Filter.cofinite (𝓝 0) }
  zero_mem' := by
    show Filter.Tendsto (fun _ : ι => (0 : 𝕜)) Filter.cofinite (𝓝 0)
    exact tendsto_const_nhds
  add_mem' := by
    intro f g hf hg
    show Filter.Tendsto (⇑(f + g)) Filter.cofinite (𝓝 0)
    have hfun : (⇑(f + g) : ι → 𝕜) = fun x => (f : ι → 𝕜) x + (g : ι → 𝕜) x := by
      funext x
      simp
    rw [hfun]
    simpa only [add_zero] using hf.add hg
  smul_mem' := by
    intro c f hf
    show Filter.Tendsto (⇑(c • f)) Filter.cofinite (𝓝 0)
    have hfun : (⇑(c • f) : ι → 𝕜) = fun x => c • (f : ι → 𝕜) x := by
      funext x
      simp [lp.coeFn_smul]
    rw [hfun]
    simpa only [smul_zero] using Filter.Tendsto.const_smul hf c

Used by 1

Used by\(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\)

AbbreviationThe sequence space \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be a type. The space \(c_0(\iota, \mathbb{K})\) consists of the functions \(x : \iota \to \mathbb{K}\) that tend to \(0\) along the cofinite filter, that is, for every \(\varepsilon > 0\) the set \(\{i : |x_i| \ge \varepsilon\}\) is finite, with pointwise operations and the supremum norm \(\|x\|_\infty = \sup_i |x_i|\). It is realized as the space of continuous functions vanishing at infinity on \(\iota\) with the discrete topology; no topology on \(\iota\) is assumed.

abbrev c0 (𝕜 : Type u) [RCLike 𝕜] (ι : Type v) : Type (max u v) :=
  @ZeroAtInftyContinuousMap ι 𝕜 ⊥ _ _

Used by 35

Used byCoordinates are bounded by the norm in \(c_0\) · Coefficients of a functional on \(c_0\) · Finite sums of the coefficients of a functional on \(c_0\) · The \(\ell^1\) coefficient sequence of a functional on \(c_0\) · The coefficients of a functional on \(c_0\) are absolutely summable · The dual of \(c_0\) is \(\ell^1\) · The \(\ell^1\)–\(c_0\) duality pairing · Formula for the \(\ell^1\)–\(c_0\) duality pairing · The \(\ell^1\)–\(c_0\) pairing as a linear map · Formula for the \(\ell^1\)–\(c_0\) pairing as a linear map · The \(\ell^1\)–\(c_0\) pairing is continuous in the \(\ell^1\) variable · The \(\ell^1\)–\(c_0\) pairing is isometric · Pairing with a unit vector is evaluation · Every functional on \(c_0\) comes from \(\ell^1\) · Coordinate evaluation on \(c_0\) · Finitely supported sequences in \(c_0\) · Coordinates of a finitely supported sequence · A functional on a finitely supported sequence · \(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\) · The \(c_0\) norm is the supremum norm · Sequences in \(\ell^\infty\) tending to zero as elements of \(c_0\) · Pairing with an \(\ell^1\) sequence as a linear functional on \(c_0\) · Value of the functional of an \(\ell^1\) sequence on \(c_0\) · Sequence supported at one index · Coordinates of the sequence supported at one index · Norm of a sequence supported at one index · Elements of \(c_0\) tend to zero along the cofinite filter · Inclusion of \(c_0\) in \(\ell^\infty\) · Finite truncation of a \(c_0\) sequence · Coordinates of a finite truncation · \(\ell^1\) norm of the coefficients of a functional on \(c_0\) · The pairing map \(\ell^1 \to c_0^*\) does not increase norms · Norm bound for the functional of an \(\ell^1\) sequence on \(c_0\) · Bound for the \(\ell^1\)–\(c_0\) pairing · Summability of the \(\ell^1\)–\(c_0\) pairing

TheoremElements of \(c_0\) tend to zero along the cofinite filter#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be an index type, and let \(c_0(\iota, \mathbb{K})\) be the space of functions \(\iota \to \mathbb{K}\) vanishing at infinity for the discrete topology on \(\iota\). For every \(x \in c_0(\iota, \mathbb{K})\), the coordinates \(x_i\) tend to \(0\) along the cofinite filter on \(\iota\).

theorem c0_tendsto_zero (x : c0 𝕜 ι) : Tendsto (x : ι → 𝕜) cofinite (𝓝 0)

Uses 1 · Used by 2

Statement usesThe sequence space \(c_0\)

Used byEvery functional on \(c_0\) comes from \(\ell^1\) · \(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\)

TheoremCoordinates are bounded by the norm in \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(c_0(\iota, \mathbb{K})\) be the space of families \(x = (x_i)_{i \in \iota}\) in \(\mathbb{K}\) that tend to \(0\) along the cofinite filter, with the supremum norm. Then \(|x_i| \le \|x\|\) for every \(x \in c_0(\iota, \mathbb{K})\) and every index \(i \in \iota\).

theorem c0_apply_norm_le (x : c0 𝕜 ι) (i : ι) : ‖(x : ι → 𝕜) i‖ ≤ ‖x‖

Uses 1 · Used by 5

Statement usesThe sequence space \(c_0\)

Used byCoordinate evaluation on \(c_0\) · The \(c_0\) norm is the supremum norm · Inclusion of \(c_0\) in \(\ell^\infty\) · Bound for the \(\ell^1\)–\(c_0\) pairing · Summability of the \(\ell^1\)–\(c_0\) pairing

DefinitionInclusion of \(c_0\) in \(\ell^\infty\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. Every \(x \in c_0(\iota, \mathbb{K})\) is a bounded sequence, and this map sends it to the element of \(\ell^\infty(\iota, \mathbb{K})\) with the same coordinates \(x_i\).

noncomputable def c0ToLp (x : c0 𝕜 ι) : lp (fun _ : ι => 𝕜) ∞ :=
  ⟨(x : ι → 𝕜), memℓp_infty ⟨‖x‖, by
    rintro _ ⟨i, rfl⟩
    exact c0_apply_norm_le x i⟩⟩

Uses 2 · Used by 4

Statement usesThe sequence space \(c_0\) · Coordinates are bounded by the norm in \(c_0\)

Used byEvery functional on \(c_0\) comes from \(\ell^1\) · \(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\) · The \(c_0\) norm is the supremum norm · Norm of a sequence supported at one index

TheoremThe \(c_0\) norm is the supremum norm#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. For every \(x \in c_0(\iota, \mathbb{K})\), the norm of \(x\) equals the norm \(\sup_{i \in \iota} |x_i|\) of \(x\) viewed as an element of \(\ell^\infty(\iota, \mathbb{K})\).

theorem c0_norm (x : c0 𝕜 ι) : ‖x‖ = ‖(x : lp (fun _ : ι => 𝕜) ∞)‖

Uses 3 · Used by 2

Statement usesThe sequence space \(c_0\) · Inclusion of \(c_0\) in \(\ell^\infty\)

Proof usesCoordinates are bounded by the norm in \(c_0\)

Used by\(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\) · Norm of a sequence supported at one index

DefinitionSequences in \(\ell^\infty\) tending to zero as elements of \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. A bounded sequence \(x \in \ell^\infty(\iota, \mathbb{K})\) whose coordinates \(x_i\) tend to \(0\) along the cofinite filter on \(\iota\) defines the element of \(c_0(\iota, \mathbb{K})\) with the same coordinates.

noncomputable def c0OfLp (x : lp (fun _ : ι => 𝕜) ∞)
    (hx : Tendsto (x : ι → 𝕜) cofinite (𝓝 0)) : c0 𝕜 ι := by
  letI : TopologicalSpace ι := ⊥
  letI : DiscreteTopology ι := ⟨rfl⟩
  exact ZeroAtInftyContinuousMap.mk
    ⟨(x : ι → 𝕜), continuous_of_discreteTopology⟩ (by
      rw [Filter.cocompact_eq_cofinite]
      exact hx)

Uses 1 · Used by 2

Statement usesThe sequence space \(c_0\)

Used by\(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\) · Sequence supported at one index

Definition\(c_0\) is isometrically isomorphic to the null sequences in \(\ell^\infty\)#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. The map that sends \(x \in c_0(\iota, \mathbb{K})\) to the same sequence \((x_i)_{i \in \iota}\), viewed in the subspace of \(\ell^\infty(\iota, \mathbb{K})\) of sequences tending to \(0\) along the cofinite filter, is a linear isometric equivalence onto that subspace.

MathlibExt.Analysis.Normed.Lp.DualC0.c0LpEquiv · 24 lines

noncomputable def c0LpEquiv : c0 𝕜 ι ≃ₗᵢ[𝕜] ↥(c0Submodule 𝕜 ι) := by
  letI : TopologicalSpace ι := ⊥
  exact
    { toFun x := ⟨(x : lp (fun _ : ι => 𝕜) ∞), c0_tendsto_zero x⟩
      invFun x := c0OfLp (x : lp (fun _ : ι => 𝕜) ∞) x.2
      left_inv x := by
        apply ZeroAtInftyContinuousMap.ext
        intro i
        rfl
      right_inv x := by
        apply Subtype.ext
        apply lp.ext
        rfl
      map_add' x y := by
        apply Subtype.ext
        apply lp.ext
        funext i
        rfl
      map_smul' c x := by
        apply Subtype.ext
        apply lp.ext
        funext i
        rfl
      norm_map' x := (c0_norm x).symm }

Uses 6

Statement usesThe sequence space \(c_0\) · Sequences in \(\ell^\infty\) tending to zero as elements of \(c_0\) · The subspace of null sequences in \(\ell^\infty\) · Inclusion of \(c_0\) in \(\ell^\infty\) · The \(c_0\) norm is the supremum norm · Elements of \(c_0\) tend to zero along the cofinite filter

DefinitionSequence supported at one index#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For an index \(i \in \iota\) and a scalar \(a \in \mathbb{K}\), this is the element of \(c_0(\iota, \mathbb{K})\) whose \(i\)-th coordinate is \(a\) and whose other coordinates are \(0\).

noncomputable def c0Single (i : ι) (a : 𝕜) : c0 𝕜 ι := by
  classical
  refine c0OfLp (lp.single ∞ i a) ?_
  have hev : (fun _ : ι => (0 : 𝕜)) =ᶠ[Filter.cofinite]
      (⇑(lp.single (E := fun _ : ι => 𝕜) ∞ i a : lp (fun _ : ι => 𝕜) ∞)) := by
    show ∀ᶠ j in Filter.cofinite, (0 : 𝕜) = (lp.single (E := fun _ : ι => 𝕜) ∞ i a) j
    rw [Filter.eventually_cofinite]
    refine Set.Finite.subset (Set.finite_singleton i) ?_
    intro j hj
    simp only [Set.mem_ofPred_eq, Set.mem_singleton_iff] at hj ⊢
    by_contra hne
    exact hj (lp.single_apply_ne (E := fun _ : ι => 𝕜) ∞ i a hne).symm
  exact Filter.Tendsto.congr' hev tendsto_const_nhds

Uses 2 · Used by 9

Statement usesThe sequence space \(c_0\) · Sequences in \(\ell^\infty\) tending to zero as elements of \(c_0\)

Used byCoefficients of a functional on \(c_0\) · Finite sums of the coefficients of a functional on \(c_0\) · The \(\ell^1\)–\(c_0\) pairing is isometric · Every functional on \(c_0\) comes from \(\ell^1\) · Finitely supported sequences in \(c_0\) · Coordinates of a finitely supported sequence · A functional on a finitely supported sequence · Coordinates of the sequence supported at one index · Norm of a sequence supported at one index

TheoremCoordinates of the sequence supported at one index#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For indices \(i, j \in \iota\) and \(a \in \mathbb{K}\), the \(j\)-th coordinate of the element of \(c_0(\iota, \mathbb{K})\) that is \(a\) at \(i\) and \(0\) elsewhere equals \(a\) if \(j = i\) and \(0\) otherwise.

theorem c0Single_apply (i j : ι) (a : 𝕜) :
    ((c0Single (𝕜 := 𝕜) (ι := ι) i a : c0 𝕜 ι) : ι → 𝕜) j = if j = i then a else 0

Uses 2 · Used by 2

Statement usesThe sequence space \(c_0\) · Sequence supported at one index

Used byThe \(\ell^1\)–\(c_0\) pairing is isometric · Coordinates of a finitely supported sequence

TheoremNorm of a sequence supported at one index#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For \(i \in \iota\) and \(a \in \mathbb{K}\), the element of \(c_0(\iota, \mathbb{K})\) that is \(a\) at \(i\) and \(0\) elsewhere has norm \(\|a\|\).

theorem c0Single_norm (i : ι) (a : 𝕜) : ‖c0Single (𝕜 := 𝕜) (ι := ι) i a‖ = ‖a‖

Uses 4

Statement usesThe sequence space \(c_0\) · Sequence supported at one index

Proof usesInclusion of \(c_0\) in \(\ell^\infty\) · The \(c_0\) norm is the supremum norm

DefinitionFinitely supported sequences in \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type, and let \(e_i \in c_0(\iota, \mathbb{K})\) be the sequence equal to \(1\) at \(i\) and \(0\) elsewhere. For a finite set \(s \subseteq \iota\) and \(c : \iota \to \mathbb{K}\), the finitely supported sequence with coefficients \(c\) on \(s\) is the element \(\sum_{i \in s} c_i e_i\) of \(c_0(\iota, \mathbb{K})\).

noncomputable def c0FinsetSum (s : Finset ι) (c : ι → 𝕜) : c0 𝕜 ι :=
  ∑ i ∈ s, c i • c0Single (𝕜 := 𝕜) (ι := ι) i (1 : 𝕜)

Uses 2 · Used by 5

Statement usesThe sequence space \(c_0\) · Sequence supported at one index

Used byFinite sums of the coefficients of a functional on \(c_0\) · Every functional on \(c_0\) comes from \(\ell^1\) · Coordinates of a finitely supported sequence · A functional on a finitely supported sequence · Finite truncation of a \(c_0\) sequence

TheoremCoordinates of a finitely supported sequence#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type, and let \(e_i \in c_0(\iota, \mathbb{K})\) be the sequence equal to \(1\) at \(i\) and \(0\) elsewhere. For every finite set \(s \subseteq \iota\), every \(c : \iota \to \mathbb{K}\) and every \(j \in \iota\), the \(j\)-th coordinate of \(\sum_{i \in s} c_i e_i\) is \(c_j\) if \(j \in s\) and \(0\) otherwise.

theorem c0FinsetSum_apply (s : Finset ι) (c : ι → 𝕜) (j : ι) :
    ((c0FinsetSum (𝕜 := 𝕜) (ι := ι) s c : c0 𝕜 ι) : ι → 𝕜) j
      = if j ∈ s then c j else 0

Uses 4 · Used by 2

Statement usesThe sequence space \(c_0\) · Finitely supported sequences in \(c_0\)

Proof usesSequence supported at one index · Coordinates of the sequence supported at one index

Used byFinite sums of the coefficients of a functional on \(c_0\) · Coordinates of a finite truncation

TheoremA functional on a finitely supported sequence#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type, and let \(e_i \in c_0(\iota, \mathbb{K})\) be the sequence equal to \(1\) at \(i\) and \(0\) elsewhere. For every continuous linear functional \(\varphi\) on \(c_0(\iota, \mathbb{K})\), every finite set \(s \subseteq \iota\) and every \(c : \iota \to \mathbb{K}\), we have \(\varphi(\sum_{i \in s} c_i e_i) = \sum_{i \in s} c_i \, \varphi(e_i)\).

theorem c0FinsetSum_apply_dual (Φ : StrongDual 𝕜 (c0 𝕜 ι)) (s : Finset ι) (c : ι → 𝕜) :
    Φ (c0FinsetSum (𝕜 := 𝕜) (ι := ι) s c) = ∑ i ∈ s, c i * Φ (c0Single i (1 : 𝕜))

Uses 3 · Used by 2

Statement usesThe sequence space \(c_0\) · Finitely supported sequences in \(c_0\) · Sequence supported at one index

Used byFinite sums of the coefficients of a functional on \(c_0\) · Every functional on \(c_0\) comes from \(\ell^1\)

DefinitionFinite truncation of a \(c_0\) sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, let \(s \subseteq \iota\) be a finite set and let \(x \in c_0(\iota, \mathbb{K})\). The truncation of \(x\) to \(s\) is the element of \(c_0(\iota, \mathbb{K})\) whose \(j\)-th coordinate is \(x_j\) for \(j \in s\) and \(0\) for \(j \notin s\); it is defined as \(\sum_{i \in s} x_i e_i\), where \(e_i\) is the sequence that is \(1\) at \(i\) and \(0\) elsewhere.

noncomputable def c0Trunc (s : Finset ι) (x : c0 𝕜 ι) : c0 𝕜 ι :=
  c0FinsetSum (𝕜 := 𝕜) (ι := ι) s (fun i => (x : ι → 𝕜) i)

Uses 2 · Used by 2

Statement usesThe sequence space \(c_0\) · Finitely supported sequences in \(c_0\)

Used byEvery functional on \(c_0\) comes from \(\ell^1\) · Coordinates of a finite truncation

TheoremCoordinates of a finite truncation#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For a finite set \(s \subseteq \iota\), an element \(x \in c_0(\iota, \mathbb{K})\) and an index \(j \in \iota\), the \(j\)-th coordinate of the truncation of \(x\) to \(s\) equals \(x_j\) if \(j \in s\) and \(0\) otherwise.

theorem c0Trunc_apply (s : Finset ι) (x : c0 𝕜 ι) (j : ι) :
    ((c0Trunc (𝕜 := 𝕜) (ι := ι) s x : c0 𝕜 ι) : ι → 𝕜) j
      = if j ∈ s then (x : ι → 𝕜) j else 0

Uses 3 · Used by 1

Statement usesThe sequence space \(c_0\) · Finite truncation of a \(c_0\) sequence

Proof usesCoordinates of a finitely supported sequence

Used byEvery functional on \(c_0\) comes from \(\ell^1\)

TheoremCoordinate norms of an \(\ell^1\) family are summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be any index type. For every \(a \in \ell^1(\iota, \mathbb{K})\), the family of norms \((\|a_i\|)_{i \in \iota}\) is summable.

theorem summable_norm_lp_one (a : lp (fun _ : ι => 𝕜) 1) :
    Summable fun i => ‖a i‖

Used by 12

Used byAssociativity of \(\ell^1\) convolution · Young's inequality with one \(\ell^1\) factor · Summability of convolution terms for \(\ell^1\) and \(\ell^p\) sequences · Summability of the Banach-space series for \(\ell^1\) convolution · Bound for the \(\ell^1\)–\(c_0\) pairing · Summability of the \(\ell^1\)–\(c_0\) pairing · Pairing \(\ell^1\) with a sequence bounded by one · Pairing with a sequence bounded by one has norm at most one · Schur's theorem · The pairing of \(\ell^1\) with sequences bounded by \(1\) is summable · Tails of an \(\ell^1\) sequence are absolutely summable · Tail of the norm series of an \(\ell^1\) sequence

TheoremSummability of the \(\ell^1\)–\(c_0\) pairing#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be a type. For every \(a \in \ell^1(\iota, \mathbb{K})\) and \(x \in c_0(\iota, \mathbb{K})\), the family \((a_i x_i)_{i \in \iota}\) is (unconditionally) summable.

theorem summable_c0Pairing (a : lp (fun _ : ι => 𝕜) 1) (x : c0 𝕜 ι) :
    Summable fun i => a i * (x : ι → 𝕜) i

Uses 3 · Used by 3

Statement usesThe sequence space \(c_0\)

Proof usesCoordinates are bounded by the norm in \(c_0\) · Coordinate norms of an \(\ell^1\) family are summable

Used byThe \(\ell^1\)–\(c_0\) pairing as a linear map · Every functional on \(c_0\) comes from \(\ell^1\) · Pairing with an \(\ell^1\) sequence as a linear functional on \(c_0\)

DefinitionPairing with an \(\ell^1\) sequence as a linear functional on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For \(a \in \ell^1(\iota, \mathbb{K})\), this is the \(\mathbb{K}\)-linear map \(c_0(\iota, \mathbb{K}) \to \mathbb{K}\) sending \(x\) to \(\sum_{i \in \iota} a_i x_i\).

noncomputable def c0PairingLin (a : lp (fun _ : ι => 𝕜) 1) : c0 𝕜 ι →ₗ[𝕜] 𝕜 where
  toFun x := ∑' i, a i * (x : ι → 𝕜) i
  map_add' x y := by
    rw [← Summable.tsum_add (summable_c0Pairing a x) (summable_c0Pairing a y)]
    refine tsum_congr fun i => ?_
    simp [ZeroAtInftyContinuousMap.coe_add, mul_add]
  map_smul' c x := by
    simp only [RingHom.id_apply, smul_eq_mul]
    rw [← tsum_mul_left]
    refine tsum_congr fun i => ?_
    simp [ZeroAtInftyContinuousMap.coe_smul, Pi.smul_apply, smul_eq_mul]
    ring

Uses 2 · Used by 3

Statement usesThe sequence space \(c_0\) · Summability of the \(\ell^1\)–\(c_0\) pairing

Used byThe \(\ell^1\)–\(c_0\) pairing as a linear map · Value of the functional of an \(\ell^1\) sequence on \(c_0\) · Bound for the \(\ell^1\)–\(c_0\) pairing

TheoremValue of the functional of an \(\ell^1\) sequence on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be an index type. For \(a \in \ell^1(\iota, \mathbb{K})\) and \(x \in c_0(\iota, \mathbb{K})\), the linear functional on \(c_0(\iota, \mathbb{K})\) given by pairing with \(a\) takes the value \(\sum_{i \in \iota} a_i x_i\) at \(x\).

theorem c0PairingLin_apply (a : lp (fun _ : ι => 𝕜) 1) (x : c0 𝕜 ι) :
    c0PairingLin (𝕜 := 𝕜) (ι := ι) a x = ∑' i, a i * (x : ι → 𝕜) i

Uses 2

Statement usesThe sequence space \(c_0\) · Pairing with an \(\ell^1\) sequence as a linear functional on \(c_0\)

TheoremBound for the \(\ell^1\)–\(c_0\) pairing#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be a type. For every \(a \in \ell^1(\iota, \mathbb{K})\) and \(x \in c_0(\iota, \mathbb{K})\), \(|\sum_{i \in \iota} a_i x_i| \le \|a\|_1 \|x\|_\infty\), where \(\|a\|_1 = \sum_i |a_i|\) and \(\|x\|_\infty = \sup_i |x_i|\).

theorem norm_c0PairingLin_le (a : lp (fun _ : ι => 𝕜) 1) (x : c0 𝕜 ι) :
    ‖c0PairingLin (𝕜 := 𝕜) (ι := ι) a x‖ ≤ ‖a‖ * ‖x‖

Uses 4 · Used by 3

Statement usesThe sequence space \(c_0\) · Pairing with an \(\ell^1\) sequence as a linear functional on \(c_0\)

Proof usesCoordinates are bounded by the norm in \(c_0\) · Coordinate norms of an \(\ell^1\) family are summable

Used byThe \(\ell^1\)–\(c_0\) pairing as a linear map · The pairing map \(\ell^1 \to c_0^*\) does not increase norms · Norm bound for the functional of an \(\ell^1\) sequence on \(c_0\)

DefinitionThe \(\ell^1\)–\(c_0\) pairing as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and let \(\ell^1(\iota, \mathbb{K})\) be the space of absolutely summable families. This is the linear map from \(\ell^1(\iota, \mathbb{K})\) to the space of continuous linear functionals on \(c_0(\iota, \mathbb{K})\) that sends \(a\) to the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\).

MathlibExt.Analysis.Normed.Lp.DualC0.c0DualPairingLin · 19 lines

noncomputable def c0DualPairingLin : lp (fun _ : ι => 𝕜) 1 →ₗ[𝕜] StrongDual 𝕜 (c0 𝕜 ι) where
  toFun a := (c0PairingLin (𝕜 := 𝕜) (ι := ι) a).mkContinuous ‖a‖ (norm_c0PairingLin_le a)
  map_add' a b := by
    apply ContinuousLinearMap.ext fun x => ?_
    simp only [add_apply, LinearMap.mkContinuous_apply, c0PairingLin_apply]
    show ∑' i, ((a + b : lp (fun _ : ι => 𝕜) 1) : ι → 𝕜) i * (x : ι → 𝕜) i
        = (∑' i, a i * (x : ι → 𝕜) i) + ∑' i, b i * (x : ι → 𝕜) i
    rw [← Summable.tsum_add (summable_c0Pairing a x) (summable_c0Pairing b x)]
    refine tsum_congr fun i => ?_
    rw [lp.coeFn_add, Pi.add_apply, add_mul]
  map_smul' c a := by
    apply ContinuousLinearMap.ext fun x => ?_
    simp only [smul_apply, LinearMap.mkContinuous_apply, c0PairingLin_apply,
      smul_eq_mul, RingHom.id_apply]
    show ∑' i, ((c • a : lp (fun _ : ι => 𝕜) 1) : ι → 𝕜) i * (x : ι → 𝕜) i
        = c * ∑' i, a i * (x : ι → 𝕜) i
    rw [← tsum_mul_left]
    refine tsum_congr fun i => ?_
    rw [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, mul_assoc]

Uses 4 · Used by 4

Statement usesThe sequence space \(c_0\) · Pairing with an \(\ell^1\) sequence as a linear functional on \(c_0\) · Bound for the \(\ell^1\)–\(c_0\) pairing · Summability of the \(\ell^1\)–\(c_0\) pairing

Used byThe \(\ell^1\)–\(c_0\) duality pairing · Formula for the \(\ell^1\)–\(c_0\) pairing as a linear map · The \(\ell^1\)–\(c_0\) pairing is continuous in the \(\ell^1\) variable · Norm bound for the functional of an \(\ell^1\) sequence on \(c_0\)

TheoremFormula for the \(\ell^1\)–\(c_0\) pairing as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and let \(\ell^1(\iota, \mathbb{K})\) be the space of absolutely summable families. For \(a \in \ell^1(\iota, \mathbb{K})\) and \(x \in c_0(\iota, \mathbb{K})\), the linear map from \(\ell^1(\iota, \mathbb{K})\) to the continuous linear functionals on \(c_0(\iota, \mathbb{K})\) given by the pairing sends \(a\) to a functional whose value at \(x\) is \(\sum_{i \in \iota} a_i x_i\). This holds by definition.

theorem c0DualPairingLin_apply (a : lp (fun _ : ι => 𝕜) 1) (x : c0 𝕜 ι) :
    c0DualPairingLin (𝕜 := 𝕜) (ι := ι) a x = ∑' i, a i * (x : ι → 𝕜) i

Uses 2 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) pairing as a linear map

Used byFormula for the \(\ell^1\)–\(c_0\) duality pairing

TheoremNorm bound for the functional of an \(\ell^1\) sequence on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be a type. For every \(a \in \ell^1(\iota, \mathbb{K})\), the image of \(a\) under the linear pairing map from \(\ell^1(\iota, \mathbb{K})\) to the continuous linear functionals on \(c_0(\iota, \mathbb{K})\), which is the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\), has operator norm at most \(\|a\|_1 = \sum_i |a_i|\).

theorem norm_c0DualPairingLin_le (a : lp (fun _ : ι => 𝕜) 1) :
    ‖c0DualPairingLin (𝕜 := 𝕜) (ι := ι) a‖ ≤ ‖a‖

Uses 3 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) pairing as a linear map

Proof usesBound for the \(\ell^1\)–\(c_0\) pairing

Used byThe \(\ell^1\)–\(c_0\) pairing is continuous in the \(\ell^1\) variable

TheoremThe \(\ell^1\)–\(c_0\) pairing is continuous in the \(\ell^1\) variable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, with the supremum norm, and let \(\ell^1(\iota, \mathbb{K})\) be the space of absolutely summable families. The linear map from \(\ell^1(\iota, \mathbb{K})\) to the space of continuous linear functionals on \(c_0(\iota, \mathbb{K})\), with the operator norm, that sends \(a\) to the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\) is continuous.

theorem c0DualPairingLin_continuous :
    Continuous (c0DualPairingLin (𝕜 := 𝕜) (ι := ι))

Uses 3 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) pairing as a linear map

Proof usesNorm bound for the functional of an \(\ell^1\) sequence on \(c_0\)

Used byThe \(\ell^1\)–\(c_0\) duality pairing

DefinitionThe \(\ell^1\)–\(c_0\) duality pairing#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. The pairing is the continuous linear map from \(\ell^1(\iota, \mathbb{K})\) to the continuous dual of \(c_0(\iota, \mathbb{K})\) that sends \(a\) to the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\).

noncomputable def c0DualPairing : lp (fun _ : ι => 𝕜) 1 →L[𝕜] StrongDual 𝕜 (c0 𝕜 ι) :=
  ContinuousLinearMap.mk c0DualPairingLin c0DualPairingLin_continuous

Uses 3 · Used by 6

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) pairing as a linear map · The \(\ell^1\)–\(c_0\) pairing is continuous in the \(\ell^1\) variable

Used byThe dual of \(c_0\) is \(\ell^1\) · Formula for the \(\ell^1\)–\(c_0\) duality pairing · The \(\ell^1\)–\(c_0\) pairing is isometric · Pairing with a unit vector is evaluation · Every functional on \(c_0\) comes from \(\ell^1\) · The pairing map \(\ell^1 \to c_0^*\) does not increase norms

TheoremFormula for the \(\ell^1\)–\(c_0\) duality pairing#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and let \(\ell^1(\iota, \mathbb{K})\) be the space of absolutely summable families. For \(a \in \ell^1(\iota, \mathbb{K})\) and \(x \in c_0(\iota, \mathbb{K})\), the canonical continuous linear map from \(\ell^1(\iota, \mathbb{K})\) to the continuous linear functionals on \(c_0(\iota, \mathbb{K})\) sends \(a\) to a functional whose value at \(x\) is \(\sum_{i \in \iota} a_i x_i\).

theorem c0DualPairing_apply (a : lp (fun _ : ι => 𝕜) 1) (x : c0 𝕜 ι) :
    c0DualPairing (𝕜 := 𝕜) (ι := ι) a x = ∑' i, a i * (x : ι → 𝕜) i

Uses 3 · Used by 4

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing

Proof usesFormula for the \(\ell^1\)–\(c_0\) pairing as a linear map

Used byThe \(\ell^1\)–\(c_0\) pairing is isometric · Pairing with a unit vector is evaluation · Every functional on \(c_0\) comes from \(\ell^1\) · The pairing map \(\ell^1 \to c_0^*\) does not increase norms

TheoremThe pairing map \(\ell^1 \to c_0^*\) does not increase norms#✓fully proved

The pairing map \(\ell^1 \to c_0^*\) does not increase norms. Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, and let \(c_0(\iota, \mathbb{K})^*\) be the space of continuous linear functionals on \(c_0(\iota, \mathbb{K})\). For every \(a \in \ell^1(\iota, \mathbb{K})\), the image of \(a\) under the continuous linear pairing map \(\ell^1(\iota, \mathbb{K}) \to c_0(\iota, \mathbb{K})^*\), which is the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\), has operator norm at most \(\|a\|_1 = \sum_i |a_i|\).

theorem norm_c0DualPairing_le (a : lp (fun _ : ι => 𝕜) 1) :
    ‖c0DualPairing (𝕜 := 𝕜) (ι := ι) a‖ ≤ ‖a‖

Uses 4 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing

Proof usesFormula for the \(\ell^1\)–\(c_0\) duality pairing · Bound for the \(\ell^1\)–\(c_0\) pairing

Used byThe \(\ell^1\)–\(c_0\) pairing is isometric

DefinitionCoefficients of a functional on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and for \(i \in \iota\) let \(e_i \in c_0(\iota, \mathbb{K})\) be the family that is \(1\) at \(i\) and \(0\) elsewhere. The coefficients of a continuous linear functional \(\Phi\) on \(c_0(\iota, \mathbb{K})\) are the family \(i \mapsto \Phi(e_i)\) in \(\mathbb{K}\).

noncomputable def c0Coeff (Φ : StrongDual 𝕜 (c0 𝕜 ι)) : ι → 𝕜 :=
  fun i => Φ (c0Single i (1 : 𝕜))

Uses 2 · Used by 3

Statement usesThe sequence space \(c_0\) · Sequence supported at one index

Used byFinite sums of the coefficients of a functional on \(c_0\) · The \(\ell^1\) coefficient sequence of a functional on \(c_0\) · The coefficients of a functional on \(c_0\) are absolutely summable

DefinitionThe normalizing scalar \(\overline{w}/|w|\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For \(w \in \mathbb{K}\), the normalizing scalar \(u(w) \in \mathbb{K}\) of \(w\) is \(0\) if \(w = 0\) and \(\overline{w}/|w|\) otherwise, so that \(u(w)\, w = |w|\).

noncomputable def c0UnitScalar (w : 𝕜) : 𝕜 :=
  if w = 0 then 0 else (starRingEnd 𝕜) w / (↑‖w‖ : 𝕜)

Used by 3

Used byFinite sums of the coefficients of a functional on \(c_0\) · The normalizing scalar times \(w\) is \(|w|\) · The normalizing scalar has absolute value at most one

TheoremThe normalizing scalar times \(w\) is \(|w|\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(w \in \mathbb{K}\), the normalizing scalar \(u(w)\) of \(w\), which is \(0\) if \(w = 0\) and \(\overline{w}/|w|\) otherwise, satisfies \(u(w)\, w = |w|\), with \(|w|\) regarded as an element of \(\mathbb{K}\).

theorem c0UnitScalar_mul (w : 𝕜) : c0UnitScalar (𝕜 := 𝕜) w * w = (↑‖w‖ : 𝕜)

Uses 1 · Used by 1

Statement usesThe normalizing scalar \(\overline{w}/|w|\)

Used byFinite sums of the coefficients of a functional on \(c_0\)

TheoremThe normalizing scalar has absolute value at most one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(w \in \mathbb{K}\), the normalizing scalar \(u(w)\) of \(w\), which is \(0\) if \(w = 0\) and \(\overline{w}/|w|\) otherwise, satisfies \(|u(w)| \le 1\).

theorem norm_c0UnitScalar_le (w : 𝕜) : ‖c0UnitScalar (𝕜 := 𝕜) w‖ ≤ 1

Uses 1 · Used by 1

Statement usesThe normalizing scalar \(\overline{w}/|w|\)

Used byFinite sums of the coefficients of a functional on \(c_0\)

TheoremFinite sums of the coefficients of a functional on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, with the supremum norm, and for \(i \in \iota\) let \(e_i \in c_0(\iota, \mathbb{K})\) be the family that is \(1\) at \(i\) and \(0\) elsewhere. For every continuous linear functional \(\Phi\) on \(c_0(\iota, \mathbb{K})\) and every finite set \(s \subseteq \iota\), we have \(\sum_{i \in s} |\Phi(e_i)| \le \|\Phi\|\), where \(\|\Phi\|\) is the operator norm.

theorem c0Coeff_finset_sum_le (Φ : StrongDual 𝕜 (c0 𝕜 ι)) (s : Finset ι) :
    ∑ i ∈ s, ‖c0Coeff (𝕜 := 𝕜) (ι := ι) Φ i‖ ≤ ‖Φ‖

Uses 9 · Used by 2

Statement usesThe sequence space \(c_0\) · Coefficients of a functional on \(c_0\)

Proof usesFinitely supported sequences in \(c_0\) · Coordinates of a finitely supported sequence · A functional on a finitely supported sequence · Sequence supported at one index · The normalizing scalar \(\overline{w}/|w|\) · The normalizing scalar times \(w\) is \(|w|\) · The normalizing scalar has absolute value at most one

Used byThe coefficients of a functional on \(c_0\) are absolutely summable · \(\ell^1\) norm of the coefficients of a functional on \(c_0\)

TheoremThe coefficients of a functional on \(c_0\) are absolutely summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and for \(i \in \iota\) let \(e_i \in c_0(\iota, \mathbb{K})\) be the family that is \(1\) at \(i\) and \(0\) elsewhere. For every continuous linear functional \(\Phi\) on \(c_0(\iota, \mathbb{K})\), the family \((\Phi(e_i))_{i \in \iota}\) lies in \(\ell^1(\iota, \mathbb{K})\), that is, \(\sum_{i \in \iota} |\Phi(e_i)| < \infty\).

theorem c0Coeff_memℓp (Φ : StrongDual 𝕜 (c0 𝕜 ι)) :
    Memℓp (c0Coeff (𝕜 := 𝕜) (ι := ι) Φ) (1 : ℝ≥0∞)

Uses 3 · Used by 1

Statement usesThe sequence space \(c_0\) · Coefficients of a functional on \(c_0\)

Proof usesFinite sums of the coefficients of a functional on \(c_0\)

Used byThe \(\ell^1\) coefficient sequence of a functional on \(c_0\)

DefinitionThe \(\ell^1\) coefficient sequence of a functional on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, and for \(i \in \iota\) let \(e_i \in c_0(\iota, \mathbb{K})\) be the family that is \(1\) at \(i\) and \(0\) elsewhere. For a continuous linear functional \(\Phi\) on \(c_0(\iota, \mathbb{K})\), this is the family \((\Phi(e_i))_{i \in \iota}\), regarded as an element of the space \(\ell^1(\iota, \mathbb{K})\) of absolutely summable families.

noncomputable def c0CoeffLp (Φ : StrongDual 𝕜 (c0 𝕜 ι)) : lp (fun _ : ι => 𝕜) 1 :=
  ⟨c0Coeff (𝕜 := 𝕜) (ι := ι) Φ, c0Coeff_memℓp Φ⟩

Uses 3 · Used by 3

Statement usesThe sequence space \(c_0\) · Coefficients of a functional on \(c_0\) · The coefficients of a functional on \(c_0\) are absolutely summable

Used byThe \(\ell^1\)–\(c_0\) pairing is isometric · Every functional on \(c_0\) comes from \(\ell^1\) · \(\ell^1\) norm of the coefficients of a functional on \(c_0\)

Theorem\(\ell^1\) norm of the coefficients of a functional on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(\Phi\) be a continuous linear functional on \(c_0(\iota, \mathbb{K})\). For \(i \in \iota\) let \(e_i\) be the sequence that is \(1\) at \(i\) and \(0\) elsewhere. The coefficient sequence \((\Phi(e_i))_{i \in \iota}\), as an element of \(\ell^1(\iota, \mathbb{K})\), has norm \(\sum_{i \in \iota} |\Phi(e_i)|\) at most the operator norm \(\|\Phi\|\).

theorem norm_c0CoeffLp_le (Φ : StrongDual 𝕜 (c0 𝕜 ι)) : ‖c0CoeffLp (𝕜 := 𝕜) (ι := ι) Φ‖ ≤ ‖Φ‖

Uses 3 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\) coefficient sequence of a functional on \(c_0\)

Proof usesFinite sums of the coefficients of a functional on \(c_0\)

Used byThe \(\ell^1\)–\(c_0\) pairing is isometric

TheoremEvery functional on \(c_0\) comes from \(\ell^1\)#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. For every continuous linear functional \(\varphi\) on \(c_0(\iota, \mathbb{K})\) there is \(a \in \ell^1(\iota, \mathbb{K})\) with \(\varphi(x) = \sum_{i \in \iota} a_i x_i\) for all \(x \in c_0(\iota, \mathbb{K})\); that is, the pairing map from \(\ell^1(\iota, \mathbb{K})\) to the continuous dual of \(c_0(\iota, \mathbb{K})\) is surjective.

The proof takes \(a_i = \varphi(e_i)\), where \(e_i\) is the sequence equal to \(1\) at \(i\) and \(0\) elsewhere, and recovers \(\varphi(x)\) as the limit of \(\varphi\) on the finite truncations of \(x\).

theorem c0DualPairing_surjective : Function.Surjective (c0DualPairing (𝕜 := 𝕜) (ι := ι))

Uses 12 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing

Proof usesThe \(\ell^1\) coefficient sequence of a functional on \(c_0\) · Formula for the \(\ell^1\)–\(c_0\) duality pairing · Finitely supported sequences in \(c_0\) · A functional on a finitely supported sequence · Sequence supported at one index · Inclusion of \(c_0\) in \(\ell^\infty\) · Finite truncation of a \(c_0\) sequence · Coordinates of a finite truncation · Elements of \(c_0\) tend to zero along the cofinite filter · Summability of the \(\ell^1\)–\(c_0\) pairing

Used byThe dual of \(c_0\) is \(\ell^1\)

TheoremThe \(\ell^1\)–\(c_0\) pairing is isometric#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. For every \(a \in \ell^1(\iota, \mathbb{K})\), the continuous linear functional \(x \mapsto \sum_{i \in \iota} a_i x_i\) on \(c_0(\iota, \mathbb{K})\), the space of sequences \(\iota \to \mathbb{K}\) tending to \(0\) at infinity with the supremum norm, has operator norm equal to \(\|a\|_1 = \sum_{i \in \iota} |a_i|\).

theorem c0DualPairing_norm (a : lp (fun _ : ι => 𝕜) 1) :
    ‖c0DualPairing (𝕜 := 𝕜) (ι := ι) a‖ = ‖a‖

Uses 8 · Used by 1

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing

Proof usesThe \(\ell^1\) coefficient sequence of a functional on \(c_0\) · Formula for the \(\ell^1\)–\(c_0\) duality pairing · Sequence supported at one index · Coordinates of the sequence supported at one index · \(\ell^1\) norm of the coefficients of a functional on \(c_0\) · The pairing map \(\ell^1 \to c_0^*\) does not increase norms

Used byThe dual of \(c_0\) is \(\ell^1\)

DefinitionThe dual of \(c_0\) is \(\ell^1\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(c_0(\iota, \mathbb{K})\) be the space of families in \(\mathbb{K}\) indexed by \(\iota\) that tend to \(0\) along the cofinite filter, with the supremum norm, and let \(\ell^1(\iota, \mathbb{K})\) be the space of absolutely summable families, with the norm \(\|a\|_1 = \sum_{i \in \iota} |a_i|\). This is the linear isometric isomorphism from \(\ell^1(\iota, \mathbb{K})\) onto the space of continuous linear functionals on \(c_0(\iota, \mathbb{K})\), with the operator norm, that sends \(a\) to the functional \(x \mapsto \sum_{i \in \iota} a_i x_i\).

noncomputable def c0DualEquiv : lp (fun _ : ι => 𝕜) 1 ≃ₗᵢ[𝕜] StrongDual 𝕜 (c0 𝕜 ι) := by
  classical
  exact LinearIsometryEquiv.ofSurjective
    ⟨(c0DualPairing (𝕜 := 𝕜) (ι := ι)).toLinearMap, fun a => c0DualPairing_norm a⟩
    c0DualPairing_surjective

Uses 4

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing · The \(\ell^1\)–\(c_0\) pairing is isometric · Every functional on \(c_0\) comes from \(\ell^1\)

DefinitionCoordinate evaluation on \(c_0\)#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type. For \(i \in \iota\), evaluation at \(i\) is the continuous linear functional \(x \mapsto x_i\) on \(c_0(\iota, \mathbb{K})\).

noncomputable def c0Eval (i : ι) : StrongDual 𝕜 (c0 𝕜 ι) :=
  (LinearMap.mkContinuous
    { toFun := fun x : c0 𝕜 ι => (x : ι → 𝕜) i
      map_add' := fun x y => by simp
      map_smul' := fun c x => by simp }
    1 fun x => by
      calc ‖(x : ι → 𝕜) i‖ ≤ ‖x‖ := c0_apply_norm_le x i
        _ = 1 * ‖x‖ := (one_mul _).symm)

Uses 2 · Used by 1

Statement usesThe sequence space \(c_0\) · Coordinates are bounded by the norm in \(c_0\)

Used byPairing with a unit vector is evaluation

TheoremPairing with a unit vector is evaluation#✓fully proved

Let \(\mathbb{K}\) be the real or complex field and \(\iota\) an index type, and for \(i \in \iota\) let \(e_i \in \ell^1(\iota, \mathbb{K})\) be the sequence equal to \(1\) at \(i\) and \(0\) elsewhere. Then the functional \(x \mapsto \sum_{j \in \iota} (e_i)_j x_j\) on \(c_0(\iota, \mathbb{K})\) given by pairing with \(e_i\) is the evaluation \(x \mapsto x_i\) at \(i\).

theorem c0DualPairing_single_eq_eval (i : ι) :
    c0DualPairing (𝕜 := 𝕜) (ι := ι) (lp.single (E := fun _ : ι => 𝕜) 1 i (1 : 𝕜))
      = c0Eval (𝕜 := 𝕜) (ι := ι) i

Uses 4

Statement usesThe sequence space \(c_0\) · The \(\ell^1\)–\(c_0\) duality pairing · Coordinate evaluation on \(c_0\)

Proof usesFormula for the \(\ell^1\)–\(c_0\) duality pairing

47 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.