Axiomatised summations

Stream: maths

[Abhimanyu Pallavi Sudhir]

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]

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

[Kenny Lau]

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]

How does this relate to tsum and has_sum that are already in mathlib?

[Patrick Massot]

Kenny explained the relation (unless tsum and has_sum can somehow be used to prove false).

[Abhimanyu Pallavi Sudhir]

...
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]

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]

No wait, that's useless.

[Kenny Lau]

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

[Abhimanyu Pallavi Sudhir]

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]

The ones that converge?

[Kenny Lau]

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

[Patrick Massot]

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

[Kenny Lau]

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]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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]

Oh wait, no it's not.

[Kevin Buzzard]

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

[Reid Barton]

maybe ∞

[Bryan Gin-ge Chen]

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]

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]

I feel like your thing works @Abhimanyu Pallavi Sudhir

[Abhimanyu Pallavi Sudhir]

Maybe. I'm playing with it.

[Kenny Lau]

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]

so the constant sequence 1 is not summable

[Kenny Lau]

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

[Kenny Lau]

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]

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]

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]

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]

boom

[Kenny Lau]

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]

#lint points out that you don't need the assumption ht.

[Kenny Lau]

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]

let's see if this new has_sum is trivial

[Kenny Lau]

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]

boom it works

[Kenny Lau]

@Abhimanyu Pallavi Sudhir there you go

[Abhimanyu Pallavi Sudhir]

Nice, thanks!

[Kenny Lau]

I have another test:

[Kenny Lau]

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

[Kenny Lau]

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

[Abhimanyu Pallavi Sudhir]

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]

good job, but you're still missing the existence

[Abhimanyu Pallavi Sudhir]

That part is just obvious, isn't it?

[Kenny Lau]

why is it obvious?

[Kenny Lau]

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

[Kenny Lau]

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]

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]

yes

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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]

one cannot just apply Godel to every situation

[Mario Carneiro]

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]

@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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Abhimanyu Pallavi Sudhir]

I think 1/(n+1) does not has_sum.

[Abhimanyu Pallavi Sudhir]

Because I cannot disprove that the "sum" of 1/(n+1) equals any given real number.

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

Specifically: the system consisting of the axioms and "sum of 1/nequalsr".

[Jeremy Avigad]

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]

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]

So existence is false.

[Kenny Lau]

why is a i linearly independent?

[Abhimanyu Pallavi Sudhir]

Isn't it?

[Abhimanyu Pallavi Sudhir]

If it isn't, there is some minimum m such that the a i up to that m are linearly dependent.

[Abhimanyu Pallavi Sudhir]

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]

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]

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

[Abhimanyu Pallavi Sudhir]

I don't. I'm just thinking.

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

What's the proof?

[Reid Barton]

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]

Ah, that's really neat.

[Kenny Lau]

nice

[Reid Barton]

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

[Koundinya Vajjha]

The hilbert matrix?

[Abhimanyu Pallavi Sudhir]

Yes!

[Koundinya Vajjha]

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

[Kenny Lau]

you guys are amazing

[Abhimanyu Pallavi Sudhir]

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]

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

[Koundinya Vajjha]

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]

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

[Kevin Buzzard]

It might be massageable into a good PLUS problem