# Axiomatic Treatment Of Sum Operators Which Work On Divergent Series

I know that various methods exist to assign values for non-converging series e.g. Cesàro summation, Hölder summation, Lambert summation, etc.

I was curious if there exists an axiomatic framework, where one looks at the set of partial operators on infinite sequences and choses a subset $$\mathcal{S}$$ of those satisfying certain axioms, then for each sequence $$a$$ one could look at the set $$\{S(a): S\in\mathcal{S}\}$$, which would even be an intervall if the axioms are deliberately chosen so that convexity of the resulting set is ensured.

One such axiom set that comes to mind would be

• Equality to $$\Sigma$$ (the 'true' sum operator) for absolute converging series (or if this is too strong, at least for finite and non-negative, converging sequences)
• Linearity (in the sense that if $$S(a)$$ and $$S(b)$$ are both defined, then $$S(\lambda a+\mu b)$$ must be defined and equal $$\lambda S(a)+\mu S(b)$$)
• Shifting the series to the right and filling in zeros from the left should not change the result
• Stability under bounded permutations (i.e. $$\pi\in S_\omega$$ is bounded if $$\forall i>0\in\mathbf{N}:|i-\pi(i)| for some $$k>0$$)

Also maybe some kind of continuity, although I don't know which metric would be apt to use on the space of sequences?

[EDIT] Now that I think about it, maybe this might just result in the interval $$[\liminf_{n\to\infty} \sum_{i, which would be boring of course.

• Note that your axioms do not prove $\sum n = -1/12$, which requires removing an infinite number of zeroes (but this has other problems). I once tried formalising something like this -- the main trouble (if we're fine with discarding $-1/12$) is in choosing the set of "summable" sequences on which the operators are defined. – Abhimanyu Pallavi Sudhir Oct 21 '19 at 11:29
• The thing is, most such proofs of sums simply assume that the given sequence is summable. E.g. when proving that such an axiomatised sum of $(1,-1,1,-1...)$ is $1/2$, you don't apply some axioms and reduce the problem to a convergent sequence -- you simply show that if it has a sum, the sum must be $1/2$. – Abhimanyu Pallavi Sudhir Oct 21 '19 at 11:32
• OK, maybe you construct a set out of those? You take some manipulation rules, possibly with parameters, and are allowed to apply them until you have some result, I wonder what would be the topological structure of the set of numbers obtained that way! – fweth Oct 21 '19 at 12:02
• By the way, why do you suspect that equality to the true sum operator may be too strong? – Abhimanyu Pallavi Sudhir Oct 21 '19 at 14:01
• I don't really suspect it, I just wrote down some ideas of how those axioms could look like... – fweth Oct 21 '19 at 14:02

EDIT:

My original answer actually defined a trivial operator -- the fixed formalisation is credit to Kenny Lau on Zulip (see the link for discussion regarding non-triviality).

import data.real.basic linear_algebra.basis data.finset
open classical
open finset

local attribute [instance, priority 0] prop_decidable

structure is_sum (Sum : (ℕ → ℝ) → ℝ → Prop) : Prop :=
(wd : ∀ {s S₁ S₂}, Sum s S₁ → Sum s S₂ → S₁ = S₂)
(sum_add : ∀ {s t S T}, Sum s S → Sum t T → Sum (λ n, s n + t n) (S + T))
(sum_smul : ∀ {s S} c, Sum s S → Sum (λ n, c * s n) (c * S))
(sum_shift : ∀ {s S}, Sum s S → Sum (λ n, s (n + 1)) (S - s 0))

def has_sum (s : ℕ → ℝ) (S : ℝ) := ∀ Sum, is_sum Sum → ∀ T, Sum s T → T = S

theorem sum_of_has_sum (s : ℕ → ℝ) (S : ℝ) (HS : has_sum s S)
(Sum : (ℕ → ℝ) → ℝ → Prop) (H : is_sum Sum) (T : ℝ) (HT : Sum s T) :
Sum s S :=
by rwa (HS Sum H T HT).symm

theorem has_sum_alt : has_sum (λ n, (-1) ^ n) (1/2) :=
begin
intros Sum HSum T HT,
have H3 := HSum.sum_shift HT,
have H2 := HSum.sum_smul (-1) HT,
have H0 := HSum.wd H2 H3,
change _ = T - 1 at H0,
linarith,
end

theorem has_sum_alt_id : has_sum (λ n, (-1) ^ n * n) (-1/4) :=
begin
intros Sum HSum T HT,
have HC : ∀ n : ℕ, (-1 : ℝ) ^ (n + 1) * (n + 1 : ℕ) + (-1) ^ n * n =
(-1) * (-1) ^ n
have H3 := HSum.sum_shift HT,
have H1 := HSum.sum_add H3 HT,
have H2 := HSum.sum_smul (-1) H1,
simp only [nat.cast_zero, mul_zero, sub_zero, HC, neg_one_mul, neg_neg] at H2,
have H4 := has_sum_alt Sum HSum _ H2,
linarith,
end

def fib : ℕ → ℝ
| 0 := 0
| 1 := 1
| (n + 2) := fib n + fib (n + 1)

theorem has_sum_fib : has_sum fib (-1) :=
have HC : ∀ n, fib n + fib (n + 1) = fib (n + 2) := λ n, rfl,
begin
intros S HSum T HT,
have H3 := HSum.sum_shift HT,
have H33 := HSum.sum_shift H3,
have H1 := HSum.sum_add HT H3,
have H0 := HSum.wd H1 H33, -- can use linearity instead of wd
simp only [fib, sub_zero] at H0,
linarith,
end

-- if a sequence has two has_sums, everything is its sum
-- (this is the case of not being summable, e.g. 1+1+1+...)
theorem has_sum_unique (s : ℕ → ℝ) (S₁ S₂ : ℝ) (H : S₁ ≠ S₂) :
has_sum s S₁ → has_sum s S₂ → ∀ S', has_sum s S' :=
λ HS₁ HS₂ T₁ Sum HSum T₂ HT₂, false.elim $$H$$ HS₂ Sum HSum S₁ \$
sum_of_has_sum s S₁ HS₁ Sum HSum T₂ HT₂

open submodule

-- a sum operator that is "forced" to give a the sum s
-- a valid sum operator iff the shifts of a are linearly independent
-- in which case a can have any sum, and thus has_sum nothing
def forced_sum (s : ℕ → ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) (S : ℝ) :
(ℕ → ℝ) → ℝ → Prop :=
λ t T, ∃ Ht : t ∈ span ℝ (set.range (λ m n : ℕ, s (n + m))),
T = finsupp.sum (linear_independent.repr H ⟨t, Ht⟩)
(λ n r, r * (S - (finset.range n).sum s))

-- linear algebra lemma
lemma spanning_set_subset_span
{R M : Type} [ring R] [add_comm_group M] [module R M] {s : set M} :
s ⊆ span R s :=
span_le.mp (le_refl _)

-- finsupp lemma
lemma finsupp.mul_sum'
{α : Type} {β : Type} {γ : Type} [_inst_1 : semiring β] [_inst_2 : semiring γ]
(b : γ) (s : α →₀ β) {f : α → β → γ} (Hf0 : ∀ a, f a 0 = 0)
(Hfa : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) :
b * finsupp.sum s f = finsupp.sum s (λ (a : α) (c : β), b * f a c) :=
begin
apply finsupp.induction s,
{ rw [finsupp.sum_zero_index, finsupp.sum_zero_index, mul_zero] },
intros A B t Ht HB IH,
finsupp.sum_single_index, finsupp.sum_single_index],
rw [Hf0, mul_zero],
exact Hf0 _,
exact λ a, by rw [Hf0, mul_zero],
intros a b₁ b₂, rw [Hfa, mul_add],
exact Hfa
end

-- finsupp lemma (another one)
lemma function_finsupp_sum (a : ℕ →₀ ℝ) (f : ℕ → ℕ → ℝ → ℝ) (k : ℕ)
(H0 : ∀ a b, f a b 0 = 0) (Hl : ∀ a b c₁ c₂, f a b (c₁ + c₂) = f a b c₁ + f a b c₂) :
(finsupp.sum a (λ m am, (λ n, f n m am))) k = finsupp.sum a (λ m am, f k m am) :=
begin
apply finsupp.induction a,
{ simp only [finsupp.sum_zero_index], refl },
intros t v a ht hv H,
finsupp.sum_single_index, finsupp.sum_single_index],
{ show f k t v + _ = f k t v + _, rw H },
{ exact H0 _ _ },
{ funext, apply H0 },
{ exact λ r, H0 _ _ },
{ exact Hl _ },
{ exact λ t, funext (λ x, by rw H0; refl) },
{ exact λ a b₁ b₂, funext (λ x, Hl _ _ _ _) }
end

-- show that forced_sum_actually does what we want
lemma forced_sum_val (s : ℕ → ℝ) (S : ℝ)
(H : linear_independent ℝ (λ m n : ℕ, s (n + m))) :
forced_sum s H S s S :=
begin
have Hs₁ : s ∈ set.range (λ m n : ℕ, s (n + m)) := set.mem_range.mpr ⟨0, rfl⟩,
have Hs₂ : s ∈ span ℝ (set.range (λ m n : ℕ, s (n + m))) :=
spanning_set_subset_span Hs₁,
have Hs₃ : (linear_independent.repr H) ⟨s, Hs₂⟩ = finsupp.single 0 1 :=
linear_independent.repr_eq_single H 0 ⟨s, Hs₂⟩ rfl,
use Hs₂, simp [Hs₃, finsupp.sum_single_index],
end

-- forced_sum is a sum: some lemmas for the hard part
noncomputable def shift_repr
(s t : ℕ → ℝ) (Ht : t ∈ span ℝ ((λ (m n : ℕ), s (n + m)) '' set.univ)) :
ℕ →₀ ℝ :=
have trep : _ := (finsupp.mem_span_iff_total ℝ).mp Ht,
finsupp.map_domain (λ x, x + 1) (classical.some trep)

def shift_repr_prop
(s t : ℕ → ℝ) (Ht : t ∈ span ℝ ((λ (m n : ℕ), s (n + m)) '' set.univ)) :
finsupp.sum (shift_repr s t Ht) (λ (m : ℕ) (am : ℝ) (n : ℕ), am * s (n + m)) =
λ (n : ℕ), t (n + 1) :=
have trep : _ := (finsupp.mem_span_iff_total ℝ).mp Ht,
let a : _ := classical.some trep in
let b : _ := shift_repr s t Ht in
have Ha : finsupp.sum a (λ (m : ℕ) (am : ℝ) (n : ℕ), am * s (n + m)) = t :=
classical.some_spec (classical.some_spec trep),
begin
have Hn : ∀ n, (finsupp.sum a (λ (m : ℕ) (am : ℝ) (n : ℕ), am * s (n + m))) n =
t n
:= by rw Ha; exact λ n, rfl,
have Hn' : ∀ (n : ℕ), finsupp.sum a (λ (m : ℕ) (am : ℝ), am * s (n + m)) = t n,
intro n,
rw [←(function_finsupp_sum a _ n _ _), Ha],
exact λ m n, zero_mul _,
exact λ m n q r, add_mul _ _ _,
have Hb : ∀ n, finsupp.sum b (λ m bm, bm * s (n + m)) =
finsupp.sum a (λ m am, am * s (n + 1 + m))
:= by
{ intro n,
convert @finsupp.sum_map_domain_index ℕ ℝ _ ℕ _ _ (λ x, x + 1) a _ _ _,
exact funext (λ m, funext (λ am, by rw [add_assoc, add_comm 1 m])),
exact λ a, zero_mul _,
exact λ n r s, add_mul _ _ _ },
have YAY := λ n, Hn' (n + 1),
have YAY' :
∀ (n : ℕ), finsupp.sum b (λ (m : ℕ) (am : ℝ), am * s (n + m)) = t (n + 1)
:= λ n, by rw [Hb, YAY],
have YAY'' : (λ n, finsupp.sum b (λ (m : ℕ) (am : ℝ), am * s (n + m))) =
(λ n, t (n + 1))
:= funext (λ n, YAY' n),
have primr : (λ n, finsupp.sum b (λ m am, am * s (n + m))) =
(finsupp.sum b (λ m am n, am * s (n + m)))
:= by
{ apply funext, intro n, apply (function_finsupp_sum b _ n _ _).symm,
exact λ m n, zero_mul _,
exact λ m n q r, add_mul _ _ _ },
rw primr at YAY'',
exact YAY'',
end

lemma shift_mem_span_shifts
(s t : ℕ → ℝ) (Ht : t ∈ span ℝ (set.range (λ (m n : ℕ), s (n + m)))) :
(λ n, t (n + 1)) ∈ span ℝ (set.range (λ (m n : ℕ), s (n + m))) :=
begin
rw set.image_univ.symm at Ht ⊢,
let b := shift_repr s t Ht,
have Hb := shift_repr_prop s t Ht,
exact (finsupp.mem_span_iff_total _).mpr
⟨b, ⟨(by rw finsupp.supported_univ; exact submodule.mem_top), by rw ←Hb; refl⟩⟩,
end

lemma forced_sum_shift
(s : ℕ → ℝ) (S : ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) :
∀ {t T}, (forced_sum s H S) t T → (forced_sum s H S) (λ n, t (n + 1)) (T - t 0) :=
λ t T ⟨Ht, HT⟩,
begin
use shift_mem_span_shifts s t Ht,

end

-- forced_sum is a sum
lemma is_sum_forced_sum (s : ℕ → ℝ) (S : ℝ)
(H : linear_independent ℝ (λ m n : ℕ, s (n + m))) :
is_sum (forced_sum s H S) :=
⟨ λ t T₁ T₂ ⟨Ht₁, HT₁⟩ ⟨Ht₂, HT₂⟩, by rw [HT₁, HT₂],
λ t₁ t₂ T₁ T₂ ⟨Ht₁, HT₁⟩ ⟨Ht₂, HT₂⟩,
begin
change _ = finsupp.sum ((linear_independent.repr H) ⟨t₁ + t₂, _⟩) _,
: (linear_independent.repr H) ⟨t₁ + t₂, _⟩ =
(linear_independent.repr H) _ + (linear_independent.repr H) _
:= (linear_independent.repr H).add ⟨t₁, Ht₁⟩ ⟨t₂, Ht₂⟩,
{ intro a, apply zero_mul },
{ intros a b c, apply add_mul }
end,
λ t T c ⟨Ht, HT⟩,
begin
use smul_mem _ c Ht,
have Hsmul
: (linear_independent.repr H) ⟨λ n, c * t n, _⟩  =
c • (linear_independent.repr H) _
:= (linear_independent.repr H).smul c ⟨t, Ht⟩,
rw [Hsmul, finsupp.sum_smul_index], simp only [mul_assoc],
rw [←finsupp.mul_sum', HT],
exact λ i, (zero_mul _),
exact λ a b c, add_mul _ _ _,
exact λ i, (zero_mul _)
end,
-- we've already done the hard part
λ t T, forced_sum_shift s S H ⟩

theorem no_sum_of_lin_ind_shifts
(s : ℕ → ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) :
∀ S : ℝ, ¬ has_sum s S :=
λ S HS,
have X : _ := HS (forced_sum s H (S + 1)) (is_sum_forced_sum s (S + 1) H) (S + 1)
(forced_sum_val s (S + 1) H),
by linarith

-- CHALLENGE: formalise the proof here:
-- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/
-- topic/Axiomatised.20summations/near/178884724
-- REQUIRES GENERATING FUNCTIONS, TAYLOR SERIES -- not currently in Lean!
theorem inv_shifts_lin_ind : linear_independent ℝ (λ m n : ℕ, 1 / (n + m + 1)) :=
begin

end


Feel free to play with it yourself. And check out the challenge (proving that there exists a sequence that does not have a sum (see the proof in math here). Actually providing an example (e.g. $$1/n$$) may be quite hard (the proof in the chat uses generating functions, which should be hard in Lean), but proving that a sequence with linearly independent shifts has no sum is almost done -- you just need to prove that the forced sum is a sum operator.

(Draft)

Here's something to get you started -- I wrote it in Lean, a formal proof-checker, because these things are tricky and I wanted to be completely sure I was being rigorous. I suppose we also need sum_con for convergent sums, but I'm not sure where infinite series are in the Lean math library!

[old code redacted]

• Nice, I always wanted to get into formal proof checking, that seems like a good starting point! – fweth Oct 21 '19 at 13:50
• @fweth If you're really interested in getting started with Lean, there's a nice discussion/QA forum you may be interested in. – Abhimanyu Pallavi Sudhir Oct 21 '19 at 13:55

Just some more thoughts:

The generalization of my proposal is that we have the following data:

• Sets $$S,T$$
• For each $$n\in\mathbf{N}$$ a set $$F_n$$ of pairs $$(f_S:S^n\to S,f_T:T^n\to T)$$

We are looking at the set $$F$$ of partial functions $$f:\text{Dom}(f)\subseteq S\to T$$ satisfying $$f(s)=t$$ whenever there is $$(f_S,f_T)\in F_n$$ and $$s_1,\dots,s_n\in\text{Dom}(f)$$ such that $$(f_S(s_1,\dots,s_n),f_T(f(s_1),\dots,f(s_n)))=(s,t).$$ I define $$F(s)$$ as $$\{t\in T:\exists f\in F.f(s)=t\}$$.

In our concrete case, $$S$$ would correspond to the set of real sequences, $$T$$ to the set of real numbers, $$F_0$$ to the set of $$(()\mapsto s,()\mapsto\sum s)$$ for each absolute converging sequence s, $$F_1$$ to the set of $$(X,\text{id})$$ for $$X$$ any bounded permutation or shifting operator and $$F_2$$ to the set of $$((s,s')\mapsto \lambda s+\mu s',(t,t')\mapsto \lambda t+\mu t')$$ for any real $$\lambda,\mu$$.

Now assume $$s\in S$$ with $$t_0,t_1\in F(s)$$ and $$t_0\neq t_1$$, I'd like to show $$F(s)=T$$ (i.e. that $$F$$ produces only trivial sets, different to what I initially expected).

Let $$\Sigma_F$$ denote the set of pairs $$(\sigma_S,\sigma_T)$$ where $$\sigma_S$$ is a formal term built recursively out of function symbols in the $$F_n$$ (possibly with holes), e.g. if $$f_S\in F_0, f'_S\in F_1 and f''_S\in F_2$$ then $$f''_S(f_S(),f'_S(\cdot))$$ and $$\cdot$$ would be such terms, and let $$\sigma_T$$ be the $$T$$-counterpart to $$\sigma_S$$. If all holes are filled with the same element $$s$$ resp. $$t$$, we write $$\sigma_S[s]$$ resp. $$\sigma_T[t]$$ for the evaluation.

Here I skip a few steps, but what I need is that for every $$\sigma_S,\sigma'_S$$ with $$\sigma_S[s]=\sigma'_S[s]$$ I have $$\sigma_T[t]=\sigma'_T[t]$$ for all $$t\in T$$, given that $$\sigma_T[t_0]=\sigma'_T[t_0]$$ and $$\sigma'_T[t_1]=\sigma'_T[t_1]$$.

I don't know how to infer the result in the abstract setting, but for the concrete case I think any $$\sigma_S[s]$$ can be described as the sequence $$s_a+\sum_{i where $$s_a$$ is absolute convergent the $$X_i$$ are operators which first shift the sequence by a finite number to the right and then perform a bounded permutation. The corresponding $$\sigma_T[t]$$ then should be $$t\mapsto\sum s_a+t\sum_{i. Let $$\sigma'_S[s]$$ resp. $$\sigma'_T[t]$$ be described as $$s'_a+\sum_{i resp. $$\sum s'+t\sum_{i. The right part of these equations is linar and since $$t_0\neq t_1$$ we can deduce $$\sum s=\sum s'$$ and $$\sum_{i. W.l.o.g. $$t_0>0$$ so for any $$t=\mu t_0$$ we have $$\sigma_T[t]=\sum s_a+\lambda\mu t=\sum s'_a+\lambda'\mu t=\sigma'_T[t]$$ as was to show.