## Stream: Is there code for X?

### Topic: Finite geometric series

#### 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?

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

#### Heather Macbeth (Jun 27 2020 at 15:35):

This is a possibly non-commutative ring

#### Jalex Stark (Jun 27 2020 at 15:35):

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

#### Jalex Stark (Jun 27 2020 at 15:37):

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

#### 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?

#### Reid Barton (Jun 27 2020 at 15:37):

Maybe we need some big_operators lemmas about commute

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

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

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


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

#### 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"? :)

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

#### Heather Macbeth (Jun 27 2020 at 15:57):

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

#### Heather Macbeth (Jun 27 2020 at 15:58):

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

#### Jalex Stark (Jun 27 2020 at 15:59):

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

#### 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)

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


#### Jalex Stark (Jun 27 2020 at 16:17):

do you have any need for

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


#### Reid Barton (Jun 27 2020 at 16:17):

First two are commute.add_right and commute.zero_right.

#### Jalex Stark (Jun 27 2020 at 16:17):

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

#### Jalex Stark (Jun 27 2020 at 16:18):

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

#### Reid Barton (Jun 27 2020 at 16:18):

@Yury G. Kudryashov @Chris Hughes ?

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

#### Yury G. Kudryashov (Jun 27 2020 at 18:04):

commute does not depend on finset anymore.

#### Yury G. Kudryashov (Jun 27 2020 at 18:05):

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

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

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

Nice! (-;

#### 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?

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

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

#3211

#### Heather Macbeth (Jun 28 2020 at 12:16):

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

#### 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) :=
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!

#### Kevin Buzzard (Jun 28 2020 at 20:50):

Is this a job for norm_cast?

#### 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?

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

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

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


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

#### Heather Macbeth (Jun 28 2020 at 23:03):

Works beautifully, thank you @David Wärn !

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