Zulip Chat Archive

Stream: maths

Topic: Axiomatised summations


view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 21 2019 at 15:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 21 2019 at 15:25):

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

view this post on Zulip Patrick Massot (Oct 21 2019 at 15:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 16:10):

No wait, that's useless.

view this post on Zulip Kenny Lau (Oct 21 2019 at 16:15):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:17):

The ones that converge?

view this post on Zulip Kenny Lau (Oct 21 2019 at 16:17):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:19):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:01):

Oh wait, no it's not.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Oct 21 2019 at 17:02):

maybe ∞

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:14):

I feel like your thing works @Abhimanyu Pallavi Sudhir

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:15):

Maybe. I'm playing with it.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:23):

so the constant sequence 1 is not summable

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:29):

boom

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 21 2019 at 17:31):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:33):

let's see if this new has_sum is trivial

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:53):

boom it works

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:53):

@Abhimanyu Pallavi Sudhir there you go

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 17:58):

Nice, thanks!

view this post on Zulip Kenny Lau (Oct 21 2019 at 17:59):

I have another test:

view this post on Zulip Kenny Lau (Oct 21 2019 at 18:00):

theorem has_sum_test (a :   ) : (∃! s, has_sum a s)  ( s, has_sum a s) :=
sorry

view this post on Zulip Kenny Lau (Oct 21 2019 at 18:05):

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

view this post on Zulip 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)))

view this post on Zulip Kenny Lau (Oct 21 2019 at 19:33):

good job, but you're still missing the existence

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:34):

That part is just obvious, isn't it?

view this post on Zulip Kenny Lau (Oct 21 2019 at 19:34):

why is it obvious?

view this post on Zulip Kenny Lau (Oct 21 2019 at 19:35):

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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 21 2019 at 19:40):

yes

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 21 2019 at 19:40):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 21 2019 at 21:44):

one cannot just apply Godel to every situation

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 22 2019 at 00:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:10):

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

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:11):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 22 2019 at 10:12):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:00):

So existence is false.

view this post on Zulip Kenny Lau (Oct 23 2019 at 19:02):

why is a i linearly independent?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:30):

Isn't it?

view this post on Zulip 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.

view this post on Zulip 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
...

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 23 2019 at 19:38):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:38):

I don't. I'm just thinking.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:39):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:40):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Oct 23 2019 at 19:41):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:43):

Ah, that's really neat.

view this post on Zulip Kenny Lau (Oct 23 2019 at 19:48):

nice

view this post on Zulip 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

view this post on Zulip Koundinya Vajjha (Oct 23 2019 at 19:50):

The hilbert matrix?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 19:50):

Yes!

view this post on Zulip Koundinya Vajjha (Oct 23 2019 at 19:50):

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

view this post on Zulip Kenny Lau (Oct 23 2019 at 19:50):

you guys are amazing

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 23 2019 at 19:52):

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

view this post on Zulip Koundinya Vajjha (Oct 23 2019 at 19:52):

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

This is a pretty cool proof.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2019 at 20:01):

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

view this post on Zulip 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