# Zulip Chat Archive

## Stream: maths

### Topic: Axiomatised summations

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 15:18):

Would "axiomatised" infinite sums be a useful addition to mathlib?

import data.real.basic def sum_add (sum : (ℕ → ℝ) → ℝ) := ∀ a b : ℕ → ℝ, sum (λ n, a n + b n) = sum a + sum b def sum_smul (sum : (ℕ → ℝ) → ℝ) := ∀ a : ℕ → ℝ, ∀ c : ℝ, sum (λ n, c * a n) = c * sum a def sum_shift (sum : (ℕ → ℝ) → ℝ) := ∀ a : ℕ → ℝ, sum (λ n, a (n + 1)) = sum a - a 0 def sum_axioms (sum : (ℕ → ℝ) → ℝ) : Prop := sum_add sum ∧ sum_smul sum ∧ sum_shift sum def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ sum, sum_axioms sum → ∀ t, sum a = t → t = s theorem has_sum_alt : has_sum (λ n, (-1) ^ n) (1/2) := begin intros sum axs t Ht, have H2 := axs.2.1 (λ n, (-1) ^ n) (-1), have H3 := axs.2.2 (λ n, (-1) ^ n), change sum (λ n, (-1) * _ ^ n) = _ - 1 at H3, rw [H2, Ht] at H3, linarith, end theorem has_sum_alt_id : has_sum (λ n, (-1) ^ n * n) (-1/4) := begin intros sum axs t Ht, have H1 := axs.1 (λ n, (-1) ^ n * ↑n) (λ n, (-1) * (-1) ^ n * (↑n + 1)), have H2 := axs.2.1 (λ n, (-1) ^ n) (-1), have H3 := axs.2.2 (λ n, (-1) ^ n * n), have HA : (λ n : ℕ, (-1) ^ n * (n : ℝ) + -1 * (-1) ^ n * (n + 1)) = (λ n, -1 * (-1) ^ n) := funext (λ n, by rw [mul_add, mul_one, ←add_assoc, neg_one_mul, ←neg_mul_eq_neg_mul, add_neg_self, zero_add]), change sum (λ (n : ℕ), (-1) * (-1) ^ n * (n + 1)) = sum (λ n, (-1) ^ n * n) - 1 * 0 at H3, rw [mul_zero, sub_zero, Ht] at H3, rw [HA, Ht, H3, H2, neg_one_mul, neg_eq_iff_neg_eq, eq_comm] at H1, have HB := has_sum_alt sum axs _ H1, linarith, end

#### Patrick Massot (Oct 21 2019 at 15:20):

https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/infinite_sum.lean

#### Kenny Lau (Oct 21 2019 at 15:24):

import data.real.basic def sum_add (sum : (ℕ → ℝ) → ℝ) := ∀ a b : ℕ → ℝ, sum (λ n, a n + b n) = sum a + sum b def sum_smul (sum : (ℕ → ℝ) → ℝ) := ∀ a : ℕ → ℝ, ∀ c : ℝ, sum (λ n, c * a n) = c * sum a def sum_shift (sum : (ℕ → ℝ) → ℝ) := ∀ a : ℕ → ℝ, sum (λ n, a (n + 1)) = sum a - a 0 def sum_axioms (sum : (ℕ → ℝ) → ℝ) : Prop := sum_add sum ∧ sum_smul sum ∧ sum_shift sum def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ sum, sum_axioms sum → ∀ t, sum a = t → t = s theorem no_sum (sum : (ℕ → ℝ) → ℝ) (h : sum_axioms sum) : false := ne_of_gt (sub_lt_self _ (zero_lt_one : (0:ℝ) < 1)) (h.2.2 (λ n, 1)) theorem sum_is_anything (a : ℕ → ℝ) (s : ℝ) : has_sum a s := λ s hs, false.elim $ no_sum s hs

#### Johan Commelin (Oct 21 2019 at 15:25):

How does this relate to `tsum`

and `has_sum`

that are already in mathlib?

#### Patrick Massot (Oct 21 2019 at 15:40):

Kenny explained the relation (unless `tsum`

and `has_sum`

can somehow be used to prove `false`

).

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:03):

... theorem no_sum (sum : (ℕ → ℝ) → ℝ) (h : sum_axioms sum) : false := ne_of_gt (sub_lt_self _ (zero_lt_one : (0:ℝ) < 1)) (h.2.2 (λ n, 1)) theorem sum_is_anything (a : ℕ → ℝ) (s : ℝ) : has_sum a s := λ s hs, false.elim $ no_sum s hs

Damn it, I keep screwing this up. There's got to be a correct way to define it.

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:10):

I have an idea. What if one defined axioms defining "summable spaces" as subspaces of `ℕ → ℝ`

that were (1) vector spaces and (2) closed under shifts -- then such spaces could have a definable summations even though all of `ℕ → ℝ`

does not.

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:10):

No wait, that's useless.

#### Kenny Lau (Oct 21 2019 at 16:15):

unfortunately this is a situation like measure theory: you can't have all sets be measurable

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:16):

Yes, but what would be a reasonably useful definition of the "Borel sets" here? Somehow there are some series for which you can define sums without causing any contradictions.

#### Kevin Buzzard (Oct 21 2019 at 16:17):

The ones that converge?

#### Kenny Lau (Oct 21 2019 at 16:17):

https://blog.wolfram.com/2014/08/06/the-abcd-of-divergent-series/

#### Patrick Massot (Oct 21 2019 at 16:18):

Again, why do you want to axiomatize this when we have it defined from first principles in mathlib?

#### Kenny Lau (Oct 21 2019 at 16:18):

I guess you can pick a letter from A to D and then consider the space of the summable functions under the letter

#### Kevin Buzzard (Oct 21 2019 at 16:19):

Abhi likes physics, he wants to do 1+2+3+4+...=-1/2 or whatever, right?

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:20):

-1/12 isn't really possible with these axioms. But e.g. 1-2+3-4+...=1/4 is.

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:51):

Perhaps this is better:

import data.real.basic def sum_add (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a b : ℕ → ℝ, ∀ s t : ℝ, sum a s → sum b t → sum (λ n, a n + b n) (s + t) def sum_smul (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a : ℕ → ℝ, ∀ s c : ℝ, sum a s → sum (λ n, c * a n) (c * s) def sum_shift (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a : ℕ → ℝ, ∀ s : ℝ, sum a s → sum (λ n, a (n + 1)) (s - a 0) def sum_axioms (has_sum : (ℕ → ℝ) → ℝ → Prop) : Prop := sum_add has_sum ∧ sum_smul has_sum ∧ sum_shift has_sum def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ sum, sum_axioms sum → ∀ t, sum a t → t = s

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:01):

Oh wait, no it's not.

#### Kevin Buzzard (Oct 21 2019 at 17:02):

1+1+1+1+1+... is never going to be summable to anything sensible using any convention, right?

#### Reid Barton (Oct 21 2019 at 17:02):

maybe ∞

#### Bryan Gin-ge Chen (Oct 21 2019 at 17:10):

Apparently some physicists would say it's -1/2: https://en.wikipedia.org/wiki/1_%2B_1_%2B_1_%2B_1_%2B_%E2%8B%AF

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:13):

1+1+1+1+1+... is never going to be summable to anything sensible using any convention, right?

Not with the axioms I defined, no. Contradicts stability.

#### Kenny Lau (Oct 21 2019 at 17:14):

I feel like your thing works @Abhimanyu Pallavi Sudhir

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:15):

Maybe. I'm playing with it.

#### Kenny Lau (Oct 21 2019 at 17:23):

import data.real.basic def sum_add (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a b : ℕ → ℝ, ∀ s t : ℝ, sum a s → sum b t → sum (λ n, a n + b n) (s + t) def sum_smul (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a : ℕ → ℝ, ∀ s c : ℝ, sum a s → sum (λ n, c * a n) (c * s) def sum_shift (sum : (ℕ → ℝ) → ℝ → Prop) := ∀ a : ℕ → ℝ, ∀ s : ℝ, sum a s → sum (λ n, a (n + 1)) (s - a 0) def sum_axioms (has_sum : (ℕ → ℝ) → ℝ → Prop) : Prop := sum_add has_sum ∧ sum_smul has_sum ∧ sum_shift has_sum def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ sum, sum_axioms sum → ∀ t, sum a t → t = s theorem sum_const_one (s : ℝ) : ¬has_sum (λ n, 1) s := assume h : has_sum (λ n, 1) s, have h1 : _ := h (λ a t, ∀ n, a n = a 0) ⟨λ a b t u ht hu n, by simp only [ht n, hu n], λ a t c ht n, by simp only [ht n], λ a s hs n, (hs (n+1)).trans (hs 1).symm⟩, have h0s : 0 = s := h1 _ $ λ n, rfl, have h1s : 1 = s := h1 _ $ λ n, rfl, zero_ne_one $ h0s.trans h1s.symm

#### Kenny Lau (Oct 21 2019 at 17:23):

so the constant sequence 1 is not summable

#### Kenny Lau (Oct 21 2019 at 17:23):

and it's a (relatively) non-trivial theorem

#### Kenny Lau (Oct 21 2019 at 17:24):

however I'm more concerned about the validity of:

theorem sum_unique (a : ℕ → ℝ) (s t : ℝ) (hs : has_sum a s) (ht : has_sum a t) : s = t := sorry

#### Kenny Lau (Oct 21 2019 at 17:27):

wait, this is troublesome:

theorem sum_const (c : ℝ) (s : ℝ) : ¬has_sum (λ n, c) s := assume h : has_sum (λ n, c) s, have h1 : _ := h (λ a t, ∀ n, a n = a 0) ⟨λ a b t u ht hu n, by simp only [ht n, hu n], λ a t c ht n, by simp only [ht n], λ a s hs n, (hs (n+1)).trans (hs 1).symm⟩, have h0s : 0 = s := h1 _ $ λ n, rfl, have h1s : 1 = s := h1 _ $ λ n, rfl, zero_ne_one $ h0s.trans h1s.symm

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:28):

however I'm more concerned about the validity of:

theorem sum_unique (a : ℕ → ℝ) (s t : ℝ) (hs : has_sum a s) (ht : has_sum a t) : s = t := sorry

It's not true. If `a`

has no sum, it has every sum. Which is why I said "oh wait it's not" earlier.

#### Kenny Lau (Oct 21 2019 at 17:29):

theorem sum_is_nothing (a : ℕ → ℝ) (s : ℝ) : ¬has_sum a s := assume h : has_sum a s, have h1 : _ := h (λ _ _, true) (by refine ⟨λ _, _, λ _, _, λ _, _⟩; intros; trivial), have h0s : 0 = s := h1 _ trivial, have h1s : 1 = s := h1 _ trivial, zero_ne_one $ h0s.trans h1s.symm

#### Kenny Lau (Oct 21 2019 at 17:29):

boom

#### Kenny Lau (Oct 21 2019 at 17:30):

theorem sum_unique (a : ℕ → ℝ) (s t : ℝ) (hs : has_sum a s) (ht : has_sum a t) : s = t := (sum_is_nothing _ _ hs).elim

#### Johan Commelin (Oct 21 2019 at 17:31):

`#lint`

points out that you don't need the assumption `ht`

.

#### Kenny Lau (Oct 21 2019 at 17:33):

I'll even propose a fix for you:

import data.real.basic structure is_sum (f : (ℕ → ℝ) → ℝ → Prop) : Prop := (wd : ∀ {a s t}, f a s → f a t → s = t) (sum_add : ∀ {a b s t}, f a s → f b t → f (λ n, a n + b n) (s + t)) (sum_smul : ∀ {a s c}, f a s → f (λ n, c * a n) (c * s)) (sum_shift : ∀ {a s}, f a s → f (λ n, a (n+1)) (s - a 0)) def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ f, is_sum f → ∀ t, f a t → t = s

#### Kenny Lau (Oct 21 2019 at 17:33):

let's see if this new `has_sum`

is trivial

#### Kenny Lau (Oct 21 2019 at 17:53):

import data.real.basic structure is_sum (f : (ℕ → ℝ) → ℝ → Prop) : Prop := (wd : ∀ {a s t}, f a s → f a t → s = t) (sum_add : ∀ {a b s t}, f a s → f b t → f (λ n, a n + b n) (s + t)) (sum_smul : ∀ {a s}, f a s → ∀ c, f (λ n, c * a n) (c * s)) (sum_shift : ∀ {a s}, f a s → f (λ n, a (n+1)) (s - a 0)) def has_sum (a : ℕ → ℝ) (s : ℝ) := ∀ f, is_sum f → ∀ t, f a t → t = s theorem has_sum_const_iff (c s : ℝ) : has_sum (λ n, c) s ↔ (c = 0 → s = 0) := ⟨λ hcs hc, eq.symm $ hcs (λ a s, (∀ n, a n = 0) ∧ s = 0) ⟨λ a s t hs ht, hs.2.trans ht.2.symm, λ a b s t hs ht, ⟨λ n, by simp only [hs.1 n, ht.1 n, add_zero], by simp only [hs.2, ht.2, add_zero]⟩, λ a s hs c, ⟨λ n, by simp only [hs.1 n, mul_zero], by simp only [hs.2, mul_zero]⟩, λ a s hs, ⟨λ n, hs.1 (n+1), by simp only [hs.2, hs.1 0, sub_zero]⟩⟩ 0 ⟨λ n, hc, rfl⟩, λ hcs f hf t hft, have htc : t = t - c := hf.1 hft (hf.4 hft), have hc0 : c = 0, by rw [← sub_sub_cancel t c, ← htc, sub_self], have ht0 : t = 0, from hf.1 hft $ by convert hf.3 hft 0; simp [hc0], ht0.trans (hcs hc0).symm⟩

#### Kenny Lau (Oct 21 2019 at 17:53):

boom it works

#### Kenny Lau (Oct 21 2019 at 17:53):

@Abhimanyu Pallavi Sudhir there you go

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:58):

Nice, thanks!

#### Kenny Lau (Oct 21 2019 at 17:59):

I have another test:

#### Kenny Lau (Oct 21 2019 at 18:00):

theorem has_sum_test (a : ℕ → ℝ) : (∃! s, has_sum a s) ∨ (∀ s, has_sum a s) := sorry

#### Kenny Lau (Oct 21 2019 at 18:05):

I don't think I can prove it. Does anyone have a counterexample?

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:33):

I can prove that.

theorem sum_of_has_sum (a : ℕ → ℝ) (s : ℝ) (H : has_sum a s) (S : (ℕ → ℝ) → ℝ → Prop) (HS : is_sum S) (t : ℝ) (Ht : S a t) : S a s := by rwa (H S HS t Ht).symm theorem has_sum_test' (a : ℕ → ℝ) (s t : ℝ) (hst : s ≠ t) : has_sum a s → has_sum a t → ∀ s, has_sum a s := λ hs ht u S HS v Hv, false.elim (hst (ht S HS s (sum_of_has_sum a s hs S HS v Hv)))

#### Kenny Lau (Oct 21 2019 at 19:33):

good job, but you're still missing the existence

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:34):

That part is just obvious, isn't it?

#### Kenny Lau (Oct 21 2019 at 19:34):

why is it obvious?

#### Kenny Lau (Oct 21 2019 at 19:35):

if the sequence is (1,0,0,0,...) then the only possible s is 1

#### Kenny Lau (Oct 21 2019 at 19:37):

and it would take me too long to prove it (I would have to construct the summation operator on finitely supported sequences)

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:39):

I'm not sure what you're saying. We just need to prove that every sequence `a`

has a real number `s`

such that `has_sum a s`

, right?

#### Kenny Lau (Oct 21 2019 at 19:40):

yes

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:40):

Well, if there wasn't, every real number would satisfy it from the definition of `has_sum`

.

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:40):

Maybe I'm confused. Let me try proving it.

#### Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:51):

Ok, yeah, it isn't obvious.

So a counter-example would be a sequence that allows multiple values of the sum without contradicting the axioms -- so then *nothing* could be its `has_sum`

.

Isn't that undecidable by Godel?

#### Kenny Lau (Oct 21 2019 at 21:44):

one cannot just apply Godel to every situation

#### Mario Carneiro (Oct 22 2019 at 00:52):

If one applies Godel to every situation, there will be situations where Godel will know something to be true but be unable to prove it (assuming Godel knows enough basic number theory)

#### Kenny Lau (Oct 22 2019 at 00:54):

@Mario Carneiro what do you think about this `has_sum`

ordeal? my algebraic knowledge is not enough to classify all subspaces of R^N closed under the shift operator

#### Reid Barton (Oct 22 2019 at 00:58):

I thought that most summation methods were not shift-invariant anyways

#### Mario Carneiro (Oct 22 2019 at 01:06):

at the very least, one of these things should come bundled with a summability predicate. All divergent series methods have one

#### Mario Carneiro (Oct 22 2019 at 01:09):

You could define a "summation method" a la https://en.wikipedia.org/wiki/Divergent_series#Properties_of_summation_methods

#### Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:10):

I think `1/(n+1)`

does not `has_sum`

.

#### Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:11):

Because I cannot disprove that the "sum" of `1/(n+1)`

equals any given real number.

#### Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:11):

But proving that no such disproof exists means proving the consistency of a system, right?

#### Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:12):

Specifically: the system consisting of the axioms and "sum of `1/n`

equals`r`

".

#### Jeremy Avigad (Oct 22 2019 at 16:42):

I have just arrived late at this party. But it sounds like the theory of Banach limits is also relevant (https://en.wikipedia.org/wiki/Banach_limit).

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 18:59):

Because I cannot disprove that the "sum" of

`1/(n+1)`

equals any given real number.

I see -- I *can* prove that the sum of `λn, 1/(n+1)`

can equal any given real number -- I just need to construct a sum operator on the smallest shift-invariant linear space of sequences containing the sequence `λn, 1/(n+1)`

Picking a basis a 1, a 2,... where `a m := λ n, 1 / (m + n)`

, it follows from basic linear algebra that defining the operator on this basis `S (a m) = x - (1 + 1/2 + ... + 1/(m-1))`

defines a sum operator for some `x`

. The key fact is that the `a i`

actually forms a basis, which is straightforward in math, but painful in Lean.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:00):

So existence is false.

#### Kenny Lau (Oct 23 2019 at 19:02):

why is `a i`

linearly independent?

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:30):

Isn't it?

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:33):

If it isn't, there is some minimum `m`

such that the `a i`

up to that `m`

are linearly dependent.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:35):

Which would produce an infinite system of linear equations:

c1 + 1/2 c2 + ... + 1/m cm = 0 1/2 c1 + 1/3 c2 + ... + 1/(m+1) cm = 0 1/3 c1 + 1/4 c2 + ... + 1/(m+2) cm = 0 ...

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:36):

In particular,

c1 + 1/2 c2 + ... + 1/m cm = 0 1/2 c1 + 1/3 c2 + ... + 1/(m+1) cm = 0 1/3 c1 + 1/4 c2 + ... + 1/(m+2) cm = 0 ... 1/(m+1) c1 + 1/(m+2) c2 + ... + 1/(2m) cm = 0

#### Reid Barton (Oct 23 2019 at 19:38):

It is linearly independent, but I'm curious to see what proof you have in mind

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:38):

I don't. I'm just thinking.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:39):

So perhaps one could work out the determinant of that system in general.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:40):

And if it's non-zero, we're done.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:41):

It is linearly independent, but I'm curious to see what proof you have in mind

What's the proof?

#### Reid Barton (Oct 23 2019 at 19:41):

If it was linearly dependent, then the sequence $a_n = 1/n$ would be defined by a linear recurrence of some fixed length and then the associated generating function $A(x) = \sum_{n \ge 1} x^n/n$ would be a rational function. But it's not, it's $-\log (1-x)$.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:43):

Ah, that's really neat.

#### Kenny Lau (Oct 23 2019 at 19:48):

nice

#### Reid Barton (Oct 23 2019 at 19:48):

I'm pretty sure the determinant you were writing down is also known, but the name escapes me at the moment

#### Koundinya Vajjha (Oct 23 2019 at 19:50):

The hilbert matrix?

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:50):

Yes!

#### Koundinya Vajjha (Oct 23 2019 at 19:50):

https://en.wikipedia.org/wiki/Hilbert_matrix

#### Kenny Lau (Oct 23 2019 at 19:50):

you guys are amazing

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:52):

I think we saw the Hilbert matrix in M1GLA @Kenny Lau -- at least if Richard Thomas taught the module for you too. We didn't calculate its determinant I think, but we did observe its invertibility.

#### Kenny Lau (Oct 23 2019 at 19:52):

even if I saw it there's no way I would remember the name

#### Koundinya Vajjha (Oct 23 2019 at 19:52):

If it was linearly dependent, then the sequence $a_n = 1/n$ would be defined by a linear recurrence of some fixed length and then the associated generating function $A(x) = \sum_{n \ge 1} x^n/n$ would be a rational function. But it's not, it's $-\log (1-x)$.

This is a pretty cool proof.

#### Abhimanyu Pallavi Sudhir (Oct 23 2019 at 20:01):

@Kevin Buzzard Would this make a good PLUS! problem?

#### Kevin Buzzard (Oct 23 2019 at 20:48):

It might be massageable into a good PLUS problem

Last updated: May 10 2021 at 08:14 UTC