Power of the sum (weak Binomial theorem)

Stream: Is there code for X?

[Xavier Xarles]

I have a (long and ugly) proof using Binomial theorem of the following result. It can be useful to show easily some results on CommSemiring.

import Mathlib.Data.Nat.Choose.Sum

variable {R : Type*}
variable [Semiring R] {x y z : R}

theorem add_pow'  (h : Commute x y) (n : ℕ) :
   ∃ z, (x + y) ^ n = x ^ n + z*y := by
  sorry

[Michael Stoll]

Use induction on n?

[Xavier Xarles]

I did. Surely can be done better.

theorem add_pow'  (h : Commute x y) (n : ℕ) :
   ∃ z, (x + y) ^ n = x ^ n + z*y := by
  induction' n with n hn
  · use 0
    rw [@pow_zero,@pow_zero,zero_mul,add_zero]
  · obtain ⟨c, hc⟩ := hn
    rw [@pow_succ']
    rw [hc]
    use c * x + x ^ n  + c * y
    rw [@add_mul,@mul_add,@mul_add,@pow_succ,@add_add_add_comm]
    rw [(pow_mul_comm' x n).symm,(distrib_three_right (c * x) (x ^ n) (c * y) y)]
    rw [(Commute.right_comm h c).symm,(add_assoc (c * x * y) (x ^ n * y) (c * y * y))]
    rw [@add_assoc]

[Xavier Xarles]

With the caps.

import Mathlib.Tactic.Linarith
import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.Group.Basic

variable {R : Type*}

variable [Semiring R] {x y z : R}

theorem add_pow'  (h : Commute x y) (n : ℕ) :
   ∃ z, (x + y) ^ n = x ^ n + z*y := by
  induction' n with n hn
  · use 0
    rw [@pow_zero,@pow_zero,zero_mul,add_zero]
  · obtain ⟨c, hc⟩ := hn
    rw [@pow_succ']
    rw [hc]
    use c * x + x ^ n  + c * y
    rw [@add_mul,@mul_add,@mul_add,@pow_succ,@add_add_add_comm]
    rw [(pow_mul_comm' x n).symm,(distrib_three_right (c * x) (x ^ n) (c * y) y)]
    rw [(Commute.right_comm h c).symm,(add_assoc (c * x * y) (x ^ n * y) (c * y * y))]
    rw [@add_assoc]

[Ruben Van de Velde]

That's better than my induction proof:

import Mathlib.Data.Nat.Choose.Sum

variable {R : Type*}
variable [Semiring R] {x y z : R}

open BigOperators

theorem add_pow'  (h : Commute x y) (n : ℕ) :
    ∃ z, (x + y) ^ n = x ^ n + z*y := by
  use (∑ m in Finset.range n, x ^ m * y ^ (n - m - 1) * (Nat.choose n m))
  rw [h.add_pow n, Finset.sum_range_succ, tsub_self, pow_zero, mul_one, Nat.choose_self, Nat.cast_one, mul_one, add_comm (x ^ n), Finset.sum_mul]
  congr 1
  refine Finset.sum_congr rfl (fun m hm => ?_)
  rw [mul_assoc _ _ y, Nat.cast_comm, ← mul_assoc, mul_assoc _ _ y, ← pow_succ', Nat.sub_add_cancel]
  simpa [Nat.succ_le] using hm

theorem add_pow''  (h : Commute x y) (n : ℕ) :
    ∃ z, (x + y) ^ n = x ^ n + z*y ∧ Commute x z ∧ Commute y z := by
  induction n with
  | zero => use 0; simp
  | succ n ih =>
    obtain ⟨z, hz, hcx, hcy⟩ := ih
    refine ⟨x ^ n + (x + y) * z, ?_, ?_, ?_⟩
    · simp only [Nat.succ_eq_add_one]
      rw [pow_succ, hz]
      rw [add_mul, mul_add]
      rw [pow_succ]
      simp_rw [add_assoc]
      congr 1
      rw [Commute.eq (a := y)]
      · rw [←mul_assoc]
        rw [← add_mul]
        congr 1
        rw [add_left_comm]
        congr 1
        rw [← hcy.eq, ← add_mul]
      · apply Commute.add_right
        apply Commute.pow_right h.symm
        apply Commute.mul_right hcy (Commute.refl _)
    · apply Commute.add_right
      apply (Commute.pow_self x n).symm
      apply Commute.mul_right ?_ hcx
      apply Commute.add_right (Commute.refl _) h
    · apply Commute.add_right
      apply Commute.pow_right h.symm
      apply Commute.mul_right ?_ hcy
      apply Commute.add_right h.symm (Commute.refl _)

theorem add_pow'''  (h : Commute x y) (n : ℕ) :
    ∃ z, (x + y) ^ n = x ^ n + z*y := by
  obtain ⟨z, hz, -⟩ := add_pow'' h n
  exact ⟨z, hz⟩

[Michael Stoll]

Xavier's proof, a bit shortened:

theorem add_pow' (h : Commute x y) (n : ℕ) : ∃ z, (x + y) ^ n = x ^ n + z*y := by
  induction' n with n hn
  · use 0
    simp
  · obtain ⟨c, hc⟩ := hn
    use c * x + x ^ n + c * y
    rw [pow_succ', hc, add_mul, mul_add, mul_add, pow_succ', add_add_add_comm, distrib_three_right,
      ← h.right_comm, add_assoc, add_assoc]

[Xavier Xarles]

I find the proof by @Ruben Van de Velde very interesting to learn how to manipulate sums. Thanks.

[Ruben Van de Velde]

Then it was worth writing :)