sum of binomial coefficients with polynomials

Stream: Is there code for X?

[Elif Uskuplu]

I'm trying to prove

lemma aux_sum (m : ℕ) (z : ℝ) : m ≥ 1 →
(∑ j : Fin (m.succ), (Nat.choose m j) * (-1)^(j :ℕ) * (z - j) ^ ((m : ℤ)-1)) = 0 := by
  sorry

to use in another result. I've checked Mathlib.Data.Nat.Choose.Sum, but couldn't find the sum involving polynomials like in here. Are there any similar results in mathlib4?

[Kevin Buzzard]

Instead of having a natural m and an assumption m>=1 and subtraction m-1 you might be better off setting t=m-1 and removing m completely and replacing it with t+1 where t is an arbitrary natural

[Elif Uskuplu]

I still need integer power, so I rewrite it as

lemma aux_sum (t : ℕ) (z : ℝ) :
  ∑ j : Fin ((t+1).succ), (Nat.choose (t+1) j) * (-1)^(j :ℕ) * (z - j) ^ (t:ℤ) = 0 := by sorry

[Elif Uskuplu]

Do you have any helper sum in mathlib4? Or I can try to prove from scratch.

[Kenny Lau]

(for others: this says $\sum_{j=0}^m C^m_j (-1)^j (z-j)^{m-1} = 0$)

[Kenny Lau]

I could have sworn I had seen this somewhere, this is about the m-th alternate difference of the power function

[Kenny Lau]

aha, i know where i saw it

[Kenny Lau]

@Elif Uskuplu a related lemma is in this PR about the forward difference

[Elif Uskuplu]

@Kenny Lau Thanks a lot, this is exactly what I'm looking for.

[Kevin Buzzard]

Why do you need integer power? Surely that gets simplified to natural power?

[Elif Uskuplu]

@Kevin Buzzard Let me explain. If it's not needed, please let me know. My mentee is working on formalizing Abel's Binomial Theorem

theorem abel_binomial {m : ℕ} : (w z : ℝ) → (hw : w ≠ 0)→
   (∑ k : Fin (m.succ), (Nat.choose m k) *
   (w + (m - k)) ^ ((m - k : ℤ) - 1) * (z + k) ^ (k : ℤ))
   = (z + w + m) ^ (m : ℤ) / w := sorry

We are trying to avoid to have situation like 0-1=0 in natural powers, so we're taking integer powers. Lemma can be coerced, but we thought that reducing somerw would be nice.

[Kevin Buzzard]

0-1=0 is natural subtraction, not natural powers. In a^b you don't have to have a and b the same type. I'm still confused

[Elif Uskuplu]

I see your confusion, and I'm not %100 sure if it is necessary. Along the proof, we have some difficulty with having natural powers and integer powers, and making all integer powers solved our issue. This is very long calc proof, I can send the draft to you as DM. We can discuss more if you're interested.

[Aaron Liu]

Natural powers and integer powers should agree where they overlap

[Elif Uskuplu]

Yes, indeed! The problem (if not mistaken) is, for example, while we're using induction on m, in the base case, we need -1 in the power of (w + (m - k)), not 0. So we set ((m - k : ℤ) - 1). In the other parts, we needed some power manipulation, so setting all powers as integer reduced the number of casting.

[Kenny Lau]

@Elif Uskuplu there might be a reason why you need Z in the main theorem, but just for the lemma you stated above, lemmas should be in the simplest (and also most general) form, and just in your lemma there was no reason to use Z.

[Kenny Lau]

Elif Uskuplu said:

I'm trying to prove

lemma aux_sum (m : ℕ) (z : ℝ) : m ≥ 1 →
(∑ j : Fin (m.succ), (Nat.choose m j) * (-1)^(j :ℕ) * (z - j) ^ ((m : ℤ)-1)) = 0 := by
  sorry

[Kenny Lau]

you have m >= 1, so m - 1 is still a natural number

[Elif Uskuplu]

Kenny Lau said:

Elif Uskuplu there might be a reason why you need Z in the main theorem, but just for the lemma you stated above, lemmas should be in the simplest (and also most general) form, and just in your lemma there was no reason to use Z.

So you mean having the version above is fine

lemma aux_sum (t : ℕ) (z : ℝ) :
  ∑ j : Fin ((t+1).succ), (Nat.choose (t+1) j) * (-1)^(j :ℕ) * (z - j) ^t = 0 := by sorry

But what happens if t is an integer in my call of aux_sum?

[Elif Uskuplu]

Oh! Forget what I'm saying. I got it now.

[Elif Uskuplu]

I assumed @Kevin Buzzard meant "it's not needed in the main theorem." Yes, if we're still talking about the lemma, I understand it wasn't needed and changed it. Thanks.

[Kenny Lau]

Elif Uskuplu said:

But what happens if t is an integer in my call of aux_sum?

what do you think the theorem should look like if t is -1?

[Kenny Lau]

also (t+1).succ is just t+2, it is not recommended to use succ like at all

[Kenny Lau]

also i think i would prefer j \in Finset.range (t+2) rather than using the Fin subtype

[Elif Uskuplu]

Kenny Lau said:

Elif Uskuplu said:

But what happens if t is an integer in my call of aux_sum?

what do you think the theorem should look like if t is -1?

aux_sum is only needed at the last step of a calc environment, I safely removed as you all suggested. -1 power is needed at the base case of the theorem since I have w^-1=1/w then. With natural power, i would have 1=1/w which is false.

[Elif Uskuplu]

@Kenny Lau Thanks for the other suggestions. I agree that the notation is not that good, I'll polish.