Zulip Chat Archive

Stream: Is there code for X?

Topic: Finite geometric series


view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:30):

I would like to use the lemma

theorem geom_sum_mul_neg [ring α] (x : α) (n : ) : (geom_series x n) * (1 - x) = 1 - x ^ n

from algebra.geom_sum, but in the "reflected" form

  (1 -x) * (geom_series x n) = 1 - x ^ n

Is there a slick way to get this, maybe using that 1 and x commute? Or do I truly need to re-prove this lemma and all the lemmas it depends on (geom_sum_mul, geom_sum₂_mul_comm, geom_sum₂_mul_add, ...) in reflected form?

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:34):

if you're writing a tactic mode proof, you can have it and then rw mul_comm at it

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:35):

This is a possibly non-commutative ring

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:35):

thanks, maybe I forgot which stream I was in :)

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:37):

hmm you could have this as a theorem about the polynomial ring Z[x] \Z[x]

view this post on Zulip Bhavik Mehta (Jun 27 2020 at 15:37):

Could you show x * geom_series x n = geom_series x n * x (using x^n * x = x * x^n) and then use distributivity perhaps?

view this post on Zulip Reid Barton (Jun 27 2020 at 15:37):

Maybe we need some big_operators lemmas about commute

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:42):

OK, for now I will just add reflected versions of a bunch of lemmas to algebra.geom_sum; hopefully Bhavik's idea will reduce my pain.

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:42):

Looks like the elegant ways also require a lot of work .. so someone else can do it later.

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:51):

This depends on #3197, which should be merged soon.

import tactic

variables (α R : Type*) [ring R] (s : finset α)

open_locale big_operators
open finset

lemma mul_sum_comm (f : α  R) (a : R) (ha :  x  s, a * f x = f x * a) :
a *  x in s, f x = ( x in s, f x) * a :=
sum_induction f (λ r, a * r = r * a)
  (λ _ _ hb hc, by rw [mul_add, add_mul, hb, hc]) (by simp) ha

view this post on Zulip Reid Barton (Jun 27 2020 at 15:52):

There is already commute which handles the parts of this other than the induction on the sum

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:53):

Heather Macbeth said:

Looks like the elegant ways also require a lot of work .. so someone else can do it later.

Wait, is this becoming "someone else can do it right now"? :)

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:55):

mm how much more are you asking to be done? this was just meant to help prove that x commutes with geom_series x n

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:57):

This counts as an elegant way, as far as I am concerned.

view this post on Zulip Heather Macbeth (Jun 27 2020 at 15:58):

By the way, is it too late to add that lemma to #3197?

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:59):

I guess not, I'm working to make it depend on commute as Reid suggested

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:59):

(I think #3197 is in a state where it will be accepted next time a reviewer notices that it has passed the linter)

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:14):

import tactic


variables {α R : Type*} [ring R] {s : finset α}

open_locale big_operators
open finset

lemma commute_add (a b c : R) (hb : commute a b) (hc : commute a c) :
commute a (b + c) :=
begin
  unfold commute, unfold semiconj_by,
  rw [mul_add, add_mul, hb.eq, hc.eq],
end

lemma commute_zero (a : R) : commute a 0 := by simp

lemma commute_sum (f : α  R) (a : R) (ha :  x  s, commute a (f x)) :
commute a ( x in s, f x) :=
sum_induction _ _ (commute_add a) (commute_zero a) ha

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:17):

do you have any need for

def commutator (a b : R) : Prop := a * b - b * a

view this post on Zulip Reid Barton (Jun 27 2020 at 16:17):

First two are commute.add_right and commute.zero_right.

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:17):

mm maybe I should have tried library_search after my eyeball-search failed

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:18):

should commute_sum go in algebra.big_operators? commute? somewhere else?

view this post on Zulip Reid Barton (Jun 27 2020 at 16:18):

@Yury G. Kudryashov @Chris Hughes ?

view this post on Zulip Chris Hughes (Jun 27 2020 at 16:48):

I would put it in commute. Probably worth proving that the set of elements that commute with a form a subring, and perhaps that the ring generated by a set of elements that commute is commutative.

view this post on Zulip Yury G. Kudryashov (Jun 27 2020 at 18:04):

commute does not depend on finset anymore.

view this post on Zulip Yury G. Kudryashov (Jun 27 2020 at 18:05):

We can define subsemiring.centralizer, then say something about sum_mem.

view this post on Zulip Yury G. Kudryashov (Jun 27 2020 at 18:05):

Or just put commute.sum_right, commute.sum_left, and commute.sum_sum into algebra.big_operators.

view this post on Zulip David Wärn (Jun 27 2020 at 18:46):

Another way of thinking about this: the desired result is algebra.geom_sum in the opposite ring docs#opposite.ring

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:53):

Nice! (-;

view this post on Zulip Reid Barton (Jun 27 2020 at 19:47):

Do we have a lemma that says that powers in the opposite ring are the same as powers in the original ring though?

view this post on Zulip David Wärn (Jun 27 2020 at 21:10):

I don't think so. Should we? Note that this is really a result about powers in the opposite monoid

view this post on Zulip Bhavik Mehta (Jun 27 2020 at 22:08):

I think that lemma should exist, since there's lemmas for mul and add so it seems odd to make users of the API implement the pow version themselves

view this post on Zulip David Wärn (Jun 28 2020 at 08:58):

#3211

view this post on Zulip Heather Macbeth (Jun 28 2020 at 12:16):

Oh, sorry, it's also in #3210 !

view this post on Zulip Heather Macbeth (Jun 28 2020 at 20:29):

By the way, here is my proof (from #3210) of the original fact.

lemma mul_geom_sum [ring α] (x : α) (n : ) :
  (x - 1) * (geom_series x n)= x ^ n - 1 :=
begin
  refine (op_inj_iff _ _).mp _,
  rw [op_mul, op_geom_series],
  have h1 : op x - 1 = op (x - 1) :=
    by rw [ op_one, sub_eq_add_neg,  op_neg,  op_add, sub_eq_add_neg],
  rw  h1,
  have h2 : op x ^ n - op 1 = op (x ^ n - 1) :=
    by { rw [sub_eq_add_neg,  op_neg,  op_pow,  op_add], refl },
  rw  h2,
  exact geom_sum_mul _ _,
end

Could this be automated? I request a tactic oppify!

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 20:50):

Is this a job for norm_cast?

view this post on Zulip Heather Macbeth (Jun 28 2020 at 20:52):

I have not used norm_cast, but the principle looks very similar. Would it work right now, or does someone need to rewrite the norm_cast tactic to include this as a suitable cast?

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 20:55):

You have to tag all the lemmas like op_add and op_one with @[norm_cast] and then you apply it and hope.

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 20:57):

I don't know what op is so I'm not 100% sure what I'm talking about, but here's an example of it all working with the coercion from the reals to the complexes. I tag a bunch of things norm_cast and then the tactic can prove "obvious" stuff. https://github.com/ImperialCollegeLondon/complex-number-game/blob/master/src/complex/Level_01_of_real.lean#L161

view this post on Zulip David Wärn (Jun 28 2020 at 20:57):

I think this is a job for simp. There's a missing lemma for subtraction

@[simp] lemma op_sub [ring α] (x y : α) : op (x - y) = op x - op y := rfl

lemma mul_geom_sum [ring α] (x : α) (n : ) :
  (x - 1) * (geom_series x n)= x ^ n - 1 :=
begin
  rw op_inj_iff,
  simpa [op_geom_series] using geom_sum_mul (op x) n,
end

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 20:59):

If simp can manage it, then great! norm_cast was developed because of Mario's insistence that simp was not a great tool for this kind of problem in general.

view this post on Zulip Heather Macbeth (Jun 28 2020 at 23:03):

Works beautifully, thank you @David Wärn !

view this post on Zulip Mario Carneiro (Jun 29 2020 at 03:01):

Kevin Buzzard said:

If simp can manage it, then great! norm_cast was developed because of Mario's insistence that simp was not a great tool for this kind of problem in general.

To clarify, simpis good if what you want to do is push all the coercions to the leaves, for example if you want to prove a theorem about nat by applying int.coe_nat_inj and then use simp to put an up arrow on every variable. If you want to do the opposite, pulling all the up arrows to the top level so they can be eliminated (like if we wanted to do the reverse of the nat -> int process just described), then simp will fight you because you are going uphill relative to simp normal form


Last updated: May 07 2021 at 21:10 UTC