The continuous dual of c₀

On a discrete index type ι, over real or complex scalars, the pairing ∑' i, a i * f i identifies absolutely summable families a ∈ ℓ¹ with continuous linear functionals on C₀(ι, 𝕜), isometrically. The inverse records the values of a functional on the unit coordinate vectors. The index type is arbitrary, including empty and uncountable types; no enumeration is chosen, and for ι = ℕ this is the classical identification c₀* = ℓ¹.

The forward map restricts Mathlib's pairing lp.dualPairing between ℓ¹ and ℓ∞ along the isometric inclusion ZeroAtInftyContinuousMap.toLpInfty of C₀(ι, 𝕜) into ℓ∞, which is defined for an arbitrary topological space α and normed group E. The pairing is bilinear, including over complex scalars: the coefficients of a functional are its values on coordinate vectors, without conjugation.

Main declarations

• ZeroAtInftyContinuousMap.toLpInfty: the inclusion of C₀(α, E) into ℓ∞, as a linear isometry.
• ZeroAtInftyContinuousMap.hasSum_apply_single_one_mul: every continuous linear functional on C₀(ι, 𝕜) is given by its coordinate series.
• ZeroAtInftyContinuousMap.sum_norm_apply_single_one_le: the coordinate values of a functional have finite partial sums of norms bounded by its norm.
• ZeroAtInftyContinuousMap.dualEquiv: the isometric equivalence ℓ¹ ≃ₗᵢ C₀(ι, 𝕜)*.
• ZeroAtInftyContinuousMap.norm_eq_tsum_norm_apply_single_one: the norm of a functional on C₀(ι, 𝕜) is the sum of the norms of its coordinate values.
• ZeroAtInftyContinuousMap.exists_forall_re_apply_eq_of_bddAbove: a real functional on C₀(ι, ℝ), read along a bounded family of points of a Banach space, is the real part of evaluation at a single point.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, Chapter 1.

def ZeroAtInftyContinuousMap.toLpInfty (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : ZeroAtInftyContinuousMap α E →ₗᵢ[𝕜] ↥(lp (fun (x : α) => E) ⊤)

The inclusion of C₀(α, E) into the bounded families ℓ∞(α, E), as a linear isometry.

@[simp]

theorem ZeroAtInftyContinuousMap.toLpInfty_apply {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : ZeroAtInftyContinuousMap α E) (x : α) : ↑((toLpInfty 𝕜) f) x = f x

The inclusion of C₀(α, E) into ℓ∞ does not change values.

theorem ZeroAtInftyContinuousMap.hasSum_apply_single_one_mul {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [SeminormedCommRing 𝕜] [DecidableEq ι] (Λ : StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)) (f : ZeroAtInftyContinuousMap ι 𝕜) : HasSum (fun (i : ι) => Λ (single i 1) * f i) (Λ f)

Every continuous linear functional on C₀(ι, 𝕜) is given by its coordinate series.

theorem ZeroAtInftyContinuousMap.sum_norm_apply_single_one_le {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (Λ : StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)) (s : Finset ι) : ∑ i ∈ s, ‖Λ (single i 1)‖ ≤ ‖Λ‖

The finite partial sums of the norms of the coordinate values of a functional on C₀(ι, 𝕜) are bounded by its norm.

theorem ZeroAtInftyContinuousMap.summable_norm_apply_single_one {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (Λ : StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)) : Summable fun (i : ι) => ‖Λ (single i 1)‖

The coordinate values of a functional on C₀(ι, 𝕜) are absolutely summable.

noncomputable def ZeroAtInftyContinuousMap.dualEquiv (𝕜 : Type u_1) (ι : Type u_2) [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] : ↥(lp (fun (x : ι) => 𝕜) 1) ≃ₗᵢ[𝕜] StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)

The isometric duality between absolutely summable scalar families and the continuous dual of C₀(ι, 𝕜). It sends a to the functional f ↦ ∑' i, a i * f i.

theorem ZeroAtInftyContinuousMap.dualEquiv_apply {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] (a : ↥(lp (fun (x : ι) => 𝕜) 1)) (f : ZeroAtInftyContinuousMap ι 𝕜) : ((dualEquiv 𝕜 ι) a) f = ∑' (i : ι), ↑a i * f i

The forward duality map is the scalar series pairing.

@[simp]

theorem ZeroAtInftyContinuousMap.dualEquiv_apply_single {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (a : ↥(lp (fun (x : ι) => 𝕜) 1)) (i : ι) (z : 𝕜) : ((dualEquiv 𝕜 ι) a) (single i z) = ↑a i * z

On a coordinate vector, the functional of a summable family is multiplication by that coordinate.

@[simp]

theorem ZeroAtInftyContinuousMap.dualEquiv_symm_apply {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (Λ : StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)) (i : ι) : ↑((dualEquiv 𝕜 ι).symm Λ) i = Λ (single i 1)

The inverse duality map records a functional's values on the unit coordinate vectors.

@[simp]

theorem ZeroAtInftyContinuousMap.dualEquiv_symm_evalCLM {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (i : ι) : (dualEquiv 𝕜 ι).symm (evalCLM 𝕜 i) = lp.single 1 i 1

The coordinate evaluations of C₀(ι, 𝕜) correspond to the unit vectors of ℓ¹.

theorem ZeroAtInftyContinuousMap.norm_eq_tsum_norm_apply_single_one {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] [DecidableEq ι] (Λ : StrongDual 𝕜 (ZeroAtInftyContinuousMap ι 𝕜)) : ‖Λ‖ = ∑' (i : ι), ‖Λ (single i 1)‖

The norm of a functional on C₀(ι, 𝕜) is the sum of the norms of its coordinate values.

theorem ZeroAtInftyContinuousMap.exists_forall_re_apply_eq_of_bddAbove {𝕜 : Type u_1} {ι : Type u_2} [TopologicalSpace ι] [DiscreteTopology ι] [RCLike 𝕜] {E : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {v : ι → E} (hv : BddAbove (Set.range fun (i : ι) => ‖v i‖)) (Λ : StrongDual ℝ (ZeroAtInftyContinuousMap ι ℝ)) : ∃ (x : E), ∀ (f : StrongDual 𝕜 E) (g : ZeroAtInftyContinuousMap ι ℝ), (∀ (i : ι), g i = RCLike.re (f (v i))) → RCLike.re (f x) = Λ g

A continuous linear functional Λ on C₀(ι, ℝ), read along a bounded family v of points of a Banach space E, is the real part of evaluation at a single point x of E: for every f : StrongDual 𝕜 E, re (f x) = Λ g whenever g is the family of the real parts of f along v. The point is ∑' i, Λ (single i 1) • v i.