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)|<k$ 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<n} a_i,\limsup_{n\to\infty} \sum_{i<n}a_i]$, which would be boring of course.

  • $\begingroup$ 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. $\endgroup$ Oct 21, 2019 at 11:29
  • $\begingroup$ 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$. $\endgroup$ Oct 21, 2019 at 11:32
  • $\begingroup$ 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! $\endgroup$
    – fweth
    Oct 21, 2019 at 12:02
  • $\begingroup$ By the way, why do you suspect that equality to the true sum operator may be too strong? $\endgroup$ Oct 21, 2019 at 14:01
  • $\begingroup$ I don't really suspect it, I just wrote down some ideas of how those axioms could look like... $\endgroup$
    – fweth
    Oct 21, 2019 at 14:02

2 Answers 2



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) :=
  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,

theorem has_sum_alt_id : has_sum (λ n, (-1) ^ n * n) (-1/4) :=
  intros Sum HSum T HT,
  have HC : ∀ n : ℕ, (-1 : ℝ) ^ (n + 1) * (n + 1 : ℕ) + (-1) ^ n * n = 
    (-1) * (-1) ^ n
  := λ n, by rw [pow_succ, nat.cast_add, mul_add, nat.cast_one, mul_one, add_comm, 
      ←add_assoc, neg_one_mul, neg_mul_eq_neg_mul_symm, add_neg_self, zero_add], 
  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,

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,
  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,

-- 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) := 
  apply finsupp.induction s,
  { rw [finsupp.sum_zero_index, finsupp.sum_zero_index, mul_zero] },
  intros A B t Ht HB IH,
  rw [finsupp.sum_add_index Hf0 _, finsupp.sum_add_index _ _, mul_add, 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

-- 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) :=
  apply finsupp.induction a,
  { simp only [finsupp.sum_zero_index], refl },
  intros t v a ht hv H,
  rw [finsupp.sum_add_index, finsupp.sum_add_index, 
    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 _ _ _ _) }

-- 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 :=
  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],

-- 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),
  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'',

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))) :=
  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⟩⟩,

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⟩, 
  use shift_mem_span_shifts s t Ht,


-- 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₂⟩, 
    use add_mem _ Ht₁ Ht₂,
    change _ = finsupp.sum ((linear_independent.repr H) ⟨t₁ + t₂, _⟩) _,
    have Hadd 
    : (linear_independent.repr H) ⟨t₁ + t₂, _⟩ = 
      (linear_independent.repr H) _ + (linear_independent.repr H) _ 
    := (linear_independent.repr H).add ⟨t₁, Ht₁⟩ ⟨t₂, Ht₂⟩, 
    rw [Hadd, HT₁, HT₂, ←finsupp.sum_add_index],
    { intro a, apply zero_mul },
    { intros a b c, apply add_mul }
  λ t T c ⟨Ht, HT⟩, 
    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 _)
  -- 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
theorem inv_shifts_lin_ind : linear_independent ℝ (λ m n : ℕ, 1 / (n + m + 1)) :=


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.



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]
  • $\begingroup$ Nice, I always wanted to get into formal proof checking, that seems like a good starting point! $\endgroup$
    – fweth
    Oct 21, 2019 at 13:50
  • 1
    $\begingroup$ @fweth If you're really interested in getting started with Lean, there's a nice discussion/QA forum you may be interested in. $\endgroup$ Oct 21, 2019 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<n} \lambda_i X_i(s)$ 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<n} \lambda_i$. Let $\sigma'_S[s]$ resp. $\sigma'_T[t]$ be described as $s'_a+\sum_{i<n}\lambda_i' X_i'(s)$ resp. $\sum s'+t\sum_{i<n}\lambda_i' t$. 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<n}\lambda_i=\sum_{i<n}\lambda_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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .