Finite geometric series

Stream: Is there code for X?

[Heather Macbeth]

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]

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

[Heather Macbeth]

This is a possibly non-commutative ring

[Jalex Stark]

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

[Jalex Stark]

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

[Bhavik Mehta]

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]

Maybe we need some big_operators lemmas about commute

[Heather Macbeth]

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]

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

[Jalex Stark]

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]

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

[Heather Macbeth]

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]

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]

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

[Heather Macbeth]

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

[Jalex Stark]

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

[Jalex Stark]

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

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

[Jalex Stark]

do you have any need for

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

[Reid Barton]

First two are commute.add_right and commute.zero_right.

[Jalex Stark]

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

[Jalex Stark]

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

[Reid Barton]

@Yury G. Kudryashov @Chris Hughes ?

[Chris Hughes]

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]

commute does not depend on finset anymore.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[David Wärn]

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

[Johan Commelin]

Nice! (-;

[Reid Barton]

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]

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

[Bhavik Mehta]

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

[David Wärn]

#3211

[Heather Macbeth]

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

[Heather Macbeth]

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!

[Kevin Buzzard]

Is this a job for norm_cast?

[Heather Macbeth]

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]

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]

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]

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]

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]

Works beautifully, thank you @David Wärn !

[Mario Carneiro]

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