Weighted geometric majorants over an index and an exponent

For a family r : ι → E in a seminormed additive group whose norms are less than one, and eventually at most 1 - ε, wherever the weight w is nonzero, the double family (i, e) ↦ w i * ‖r i‖ ^ (e + 1) is summable over ι × ℕ as soon as i ↦ w i * ‖r i‖ is summable. Each fibre is geometric, so it sums to w i * ‖r i‖ / (1 - ‖r i‖), and the eventual bound keeps 1 / (1 - ‖r i‖) under ε⁻¹ off a finite set; a fibre where the weight vanishes is zero and needs no bound at all.

Main results

• TauCeti.summable_mul_norm_pow_succ: the weighted double family is summable over ι × ℕ.

theorem TauCeti.summable_mul_norm_pow_succ {ι : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {r : ι → E} {w : ι → ℝ} (hbd : ∃ ε > 0, ∀ᶠ (i : ι) in Filter.cofinite, w i ≠ 0 → ‖r i‖ ≤ 1 - ε) (hwr : Summable fun (i : ι) => w i * ‖r i‖) (h1 : ∀ (i : ι), w i ≠ 0 → ‖r i‖ < 1) : Summable fun (ie : ι × ℕ) => w ie.1 * ‖r ie.1‖ ^ (ie.2 + 1)

A weighted geometric family is summable over index and exponent together. Let w : ι → ℝ be weights with i ↦ w i * ‖r i‖ summable, and let r be a family in a seminormed additive group which, at every index where w is nonzero, has norm less than one and eventually norm at most 1 - ε. Then the double family (i, e) ↦ w i * ‖r i‖ ^ (e + 1) is summable over ι × ℕ.

Both conditions on r are restricted to the support of w, and off that support nothing is asked of r at all: a fibre with w i = 0 is identically zero whatever r i is. The weights are unrestricted in sign, since only |w i| enters the majorant.

The eventual bound is what the fibres need — the fibre at i sums to w i * ‖r i‖ / (1 - ‖r i‖), which is comparable to w i * ‖r i‖ only where ‖r i‖ stays away from 1. Summability of r would give this, but is far stronger: it rules out a family of constant norm with summable weights.

This is the bound a termwise differentiation argument runs on whenever the differentiated terms are an index-only weight times a norm power; it says nothing on its own about which families have that form.