Phillips' lemma (Lemmas 2.2 and 2.3)

Lemma 2.2 (lem:Phillips). Let (μ_n) be a sequence in (ℓ^∞(ℕ))* such that μ_n(a) → 0 for every a ∈ ℓ^∞(ℕ). Then Σ_k |μ_n(e_k)| → 0; in particular μ_n(e_n) → 0.

Lemma 2.3 (lem:cor-Phillips). Let S ∈ 𝓛(ℓ^∞(ℕ), X) and t_n ≥ 0 with t_n → 0. Then ‖(T_{t_n} - Id) S e_n‖ → 0.

Main declarations

• Phillips.full : Lemma 2.2 (summability of each Σ_k |μ_n(e_k)|, convergence of the sums to 0, and μ_n(e_n) → 0); Phillips.tsum_abs_tendsto_zero is the real case written with absolute values.
• Phillips.uniform : Lemma 2.3. Only strong right-continuity of T at 0 is used; the semigroup law and completeness are not needed.

Linfty 𝕜 is the space of bounded sequences with values in 𝕜 = ℝ or ℂ, represented as bounded continuous functions on the discrete space ℕ; e k is the k-th canonical vector. The paper quotes Lemma 2.2 from [Phillips 1940]; here it is proved.

Proof of Lemma 2.2

1. Diagonal statement, diagonal_tendsto_zero: μ_n(e_n) → 0. An infinite set of indices is thinned so that a given functional is small on all its subsets (small_on_subsets); a recursive selection then produces a set A for which μ_n(1_A) cannot tend to zero (diagonal_of_indicator_tendsto). Only finite sums are used.
2. For a single functional, Σ_{k ∈ s} |φ(e_k)| ≤ ‖φ‖ for every finite s, by testing φ on Σ_{k ∈ s} λ_k e_k with phases |λ_k| ≤ 1 (sum_norm_eval_le); hence the series converge (summable_norm_eval).
3. Disjoint finite blocks B_j with coefficients of modulus ≤ 1 are encoded by one bounded operator S : ℓ^∞ → ℓ^∞ with S e_j supported in B_j, defined coordinatewise (exists_block_operator).
4. Gliding hump (finite_sum_eventually_small): if finite sums were not eventually uniformly small, Steps 2–3 would produce functionals ν_j = μ_{r_j} ∘ S contradicting Step 1. This gives Σ_k |μ_n(e_k)| → 0 (tsum_norm_tendsto_zero).

Lemma 2.3 (uniform) applies the diagonal statement to μ_n = x_n^* ∘ (T_{t_n} - Id) ∘ S, with norming functionals x_n^* given by Hahn–Banach (norm_diagonal_tendsto_zero).

@[reducible, inline]

abbrev AbstractLinearControl.Phillips.Linfty (𝕜 : Type u_1) [RCLike 𝕜] : Type u_1

Bounded scalar sequences, with the supremum norm.

Equations

• AbstractLinearControl.Phillips.Linfty 𝕜 = BoundedContinuousFunction ℕ 𝕜

noncomputable def AbstractLinearControl.Phillips.chi {𝕜 : Type u_1} [RCLike 𝕜] (S : Set ℕ) : Linfty 𝕜

The characteristic sequence of a set of natural numbers.

Equations

• AbstractLinearControl.Phillips.chi S = BoundedContinuousFunction.ofNormedAddCommGroupDiscrete (fun (k : ℕ) => if k ∈ S then 1 else 0) 1 ⋯

@[simp]

theorem AbstractLinearControl.Phillips.chi_apply {𝕜 : Type u_1} [RCLike 𝕜] (S : Set ℕ) (k : ℕ) : (chi S) k = if k ∈ S then 1 else 0

noncomputable def AbstractLinearControl.Phillips.e {𝕜 : Type u_1} [RCLike 𝕜] (k : ℕ) : Linfty 𝕜

The kth canonical vector of ℓ∞.

Equations

• AbstractLinearControl.Phillips.e k = AbstractLinearControl.Phillips.chi {k}

@[simp]

theorem AbstractLinearControl.Phillips.e_apply {𝕜 : Type u_1} [RCLike 𝕜] (k j : ℕ) : (e k) j = if j = k then 1 else 0

Step 1: the diagonal statement μ_n(e_n) → 0

theorem AbstractLinearControl.Phillips.diagonal_of_indicator_tendsto {𝕜 : Type u_1} [RCLike 𝕜] (μ : ℕ → Linfty 𝕜 →L[𝕜] 𝕜) (hμ : ∀ (S : Set ℕ), Filter.Tendsto (fun (n : ℕ) => (μ n) (chi S)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n) (e n)) Filter.atTop (nhds 0)

It is enough to assume convergence on characteristic sequences.

theorem AbstractLinearControl.Phillips.diagonal_tendsto_zero {𝕜 : Type u_1} [RCLike 𝕜] (μ : ℕ → Linfty 𝕜 →L[𝕜] 𝕜) (hμ : ∀ (a : Linfty 𝕜), Filter.Tendsto (fun (n : ℕ) => (μ n) a) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n) (e n)) Filter.atTop (nhds 0)

Step 1 (diagonal statement): if μ_n(a) → 0 for every a ∈ ℓ^∞, then μ_n(e_n) → 0. This is the "in particular" part of Lemma 2.2, proved first; the full lemma (Phillips.full) is deduced from it.

Step 2: finite sums Σ_{k ∈ s} |φ(e_k)| ≤ ‖φ‖

theorem AbstractLinearControl.Phillips.sum_norm_eval_le {𝕜 : Type u_1} [RCLike 𝕜] (φ : Linfty 𝕜 →L[𝕜] 𝕜) (s : Finset ℕ) : ∑ k ∈ s, ‖φ (e k)‖ ≤ ‖φ‖

Every finite sum of the absolute values of the atomic coefficients is bounded by the norm of the functional.

theorem AbstractLinearControl.Phillips.summable_norm_eval {𝕜 : Type u_1} [RCLike 𝕜] (φ : Linfty 𝕜 →L[𝕜] 𝕜) : Summable fun (k : ℕ) => ‖φ (e k)‖

The atomic coefficients of any bounded functional on ℓ∞ are in ℓ¹. This requires no convergence hypothesis on a sequence of functionals.

theorem AbstractLinearControl.Phillips.tsum_norm_eval_le {𝕜 : Type u_1} [RCLike 𝕜] (φ : Linfty 𝕜 →L[𝕜] 𝕜) : ∑' (k : ℕ), ‖φ (e k)‖ ≤ ‖φ‖

The ℓ¹ norm of the atomic coefficients is at most the operator norm.

Step 3: disjoint finite blocks, encoded by one bounded operator ℓ^∞ → ℓ^∞

Step 4: uniform smallness of all finite sums (gliding hump)

theorem AbstractLinearControl.Phillips.finite_sum_eventually_small {𝕜 : Type u_1} [RCLike 𝕜] (μ : ℕ → Linfty 𝕜 →L[𝕜] 𝕜) (hμ : ∀ (a : Linfty 𝕜), Filter.Tendsto (fun (n : ℕ) => (μ n) a) Filter.atTop (nhds 0)) (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (s : Finset ℕ), ∑ k ∈ s, ‖(μ n) (e k)‖ < ε

Eventually, Σ_{k ∈ s} |μ_n(e_k)| < ε for all finite sets s at once. Otherwise one selects late rows r_j and pairwise disjoint finite blocks B_j with Σ_{k ∈ B_j} |μ_{r_j}(e_k)| ≥ ε/2; encoding the blocks (with phases) by one operator S, the functionals ν_j = μ_{r_j} ∘ S contradict the diagonal statement of Step 1.

Lemma 2.2

theorem AbstractLinearControl.Phillips.tsum_norm_tendsto_zero {𝕜 : Type u_1} [RCLike 𝕜] (μ : ℕ → Linfty 𝕜 →L[𝕜] 𝕜) (hμ : ∀ (a : Linfty 𝕜), Filter.Tendsto (fun (n : ℕ) => (μ n) a) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∑' (k : ℕ), ‖(μ n) (e k)‖) Filter.atTop (nhds 0)

Main conclusion of Lemma 2.2: Σ_k |μ_n(e_k)| → 0 (each series converges by summable_norm_eval).

theorem AbstractLinearControl.Phillips.full {𝕜 : Type u_1} [RCLike 𝕜] (μ : ℕ → Linfty 𝕜 →L[𝕜] 𝕜) (hμ : ∀ (a : Linfty 𝕜), Filter.Tendsto (fun (n : ℕ) => (μ n) a) Filter.atTop (nhds 0)) : (∀ (n : ℕ), Summable fun (k : ℕ) => ‖(μ n) (e k)‖) ∧ Filter.Tendsto (fun (n : ℕ) => ∑' (k : ℕ), ‖(μ n) (e k)‖) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => (μ n) (e n)) Filter.atTop (nhds 0)

Lemma 2.2 (lem:Phillips, Phillips' lemma), over ℝ or ℂ. Let (μ_n) be bounded linear functionals on ℓ^∞(ℕ) with μ_n(a) → 0 for every a ∈ ℓ^∞(ℕ). Then, for every n, the series Σ_k |μ_n(e_k)| converges, Σ_k |μ_n(e_k)| → 0, and in particular μ_n(e_n) → 0.

theorem AbstractLinearControl.Phillips.tsum_abs_tendsto_zero (μ : ℕ → Linfty ℝ →L[ℝ] ℝ) (hμ : ∀ (a : Linfty ℝ), Filter.Tendsto (fun (n : ℕ) => (μ n) a) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∑' (k : ℕ), |(μ n) (e k)|) Filter.atTop (nhds 0)

Lemma 2.2 for real scalars, written with absolute values as in the paper.

Lemma 2.3

theorem AbstractLinearControl.Phillips.norm_diagonal_tendsto_zero {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (A : ℕ → Linfty 𝕜 →L[𝕜] X) (hA : ∀ (a : Linfty 𝕜), Filter.Tendsto (fun (n : ℕ) => (A n) a) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ‖(A n) (e n)‖) Filter.atTop (nhds 0)

Vector-valued version of diagonal_tendsto_zero: if A_n a → 0 for every a ∈ ℓ^∞, then ‖A_n e_n‖ → 0. (A norming functional is chosen for each A_n e_n.)

theorem AbstractLinearControl.Phillips.uniform {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : Linfty 𝕜 →L[𝕜] X) (T : ℝ → X →L[𝕜] X) (hT : ∀ (x : X), Filter.Tendsto (fun (s : ℝ) => (T s) x) (nhdsWithin 0 (Set.Ici 0)) (nhds x)) (t : ℕ → ℝ) (ht_nonneg : ∀ (n : ℕ), 0 ≤ t n) (ht : Filter.Tendsto t Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ‖(T (t n) - ContinuousLinearMap.id 𝕜 X) (S (e n))‖) Filter.atTop (nhds 0)

Lemma 2.3 (lem:cor-Phillips). Let S : ℓ^∞ → X be a bounded operator and t n ≥ 0 with t n → 0. Then ‖(T (t n) - Id) (S (e n))‖ → 0.

Only strong right-continuity of T at zero is required; the semigroup law and completeness of X are not used.