How to fix the sorry?

Stream: new members

[tsuki hao]

import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Nat.Factorial.Basic

open Nat

open Finset

open BigOperators

theorem Idt36 {n k m : ℕ} (hk : k ≤ n) (hm : m ≤ n) (hkm : m ≤ k) : (∑ k in Icc 0 n,  (choose n k) * (descFactorial (k + 1) m)) = (descFactorial (n + 1) m) * 2 ^(n - m):= by
  have h1 : (∑ k in Icc 0 n,  (choose n k) * (descFactorial (k + 1) m)) = (∑ k in Icc m n, (descFactorial (n + 1) m) * choose (n - m) (k - m)) := by
    have h2 : (choose n k) * (descFactorial (k + 1) m) = (descFactorial (n + 1) m) * choose (n - m) (k - m) := by
      sorry
    sorry
  rw[h1]
  have h3 : (∑ k in Icc m n, descFactorial (n + 1) m * Nat.choose (n - m) (k - m)) = descFactorial (k + 1) m * (∑ k in Icc m n, Nat.choose (n - m) (k - m)) := by
    sorry
  rw[h3]
  have h4 :  (∑ k in Icc m n, Nat.choose (n - m) (k - m)) = 2 ^ (n - m) := by
    sorry
  rw[h4]

Does anyone know how to fix the sorry?

[Kevin Buzzard]

There are four sorries -- which one are you asking about?

My instinct with these things is that the first thing to do is to remove all the natural subtractions by writing k=m+s and n=m+s+t and then doing all the cancellation; then you're much more likely to find lemmas in mathlib which will help you.

[tsuki hao]

Kevin Buzzard said:

There are four sorries -- which one are you asking about?

My instinct with these things is that the first thing to do is to remove all the natural subtractions by writing k=m+s and n=m+s+t and then doing all the cancellation; then you're much more likely to find lemmas in mathlib which will help you.

In fact, I am still thinking about this problem. I found a problem. If m is set to 2, then the expression of k starting from 0 seems to lose its mathematical meaning.

[Kevin Buzzard]

I am not suggesting that you relax the condition m<=k. I am suggesting that you replace k everywhere with m+x with x : Nat and replace k-m with x so as to remove all mention of natural subtraction

[Yongyi Chen]

One weird thing I noticed is that the variable $k$ and the hypotheses $k\le n$ and $m\le k$ are useless because the $k$ inside the sum is a different variable from the $k$ outside the sum.

[Winston Yin (尹維晨)]

Did you mean to impose the conditions k ≤ n and m ≤ k inside the sum, rather than outside?

[Winston Yin (尹維晨)]

Assuming that, k ≤ n is superfluous due to docs#Nat.choose_eq_zero_of_lt

[Winston Yin (尹維晨)]

Similarly, m ≤ k is superfluous as well, due to docs#Nat.descFactorial_eq_zero_iff_lt

[Winston Yin (尹維晨)]

Same for m ≤ n

[Winston Yin (尹維晨)]

I haven't worked through your problem myself, but since the definitions of choose and descFactorial are inductive, my hunch would be to use induction on n and m. The other footgun that Kevin pointed out is the n - m on the right hand side. Lean defines subtraction between two natural numbers to be 0 when the result would be negative. That's ok in your case, since descFactorial (n + 1) m would be zero as well. But it's something to look out for when writing your proof. Good luck!

[tsuki hao]

Kevin Buzzard said:

I am not suggesting that you relax the condition m<=k. I am suggesting that you replace k everywhere with m+x with x : Nat and replace k-m with x so as to remove all mention of natural subtraction

I tried this method, but failed. I think If k is represented as m+n, n:N, there is still no way to avoid this problem, because the natural numbers are non-negative.

[tsuki hao]

tsuki hao said:

Kevin Buzzard said:

I am not suggesting that you relax the condition m<=k. I am suggesting that you replace k everywhere with m+x with x : Nat and replace k-m with x so as to remove all mention of natural subtraction

I tried this method, but failed. I think If k is represented as m+n, n:N, there is still no way to avoid this problem, because the natural numbers are non-negative.

It turns out that the negative number will be 0, I will continue to try!

[tsuki hao]

Winston Yin (尹維晨) said:

I haven't worked through your problem myself, but since the definitions of choose and descFactorial are inductive, my hunch would be to use induction on n and m. The other footgun that Kevin pointed out is the n - m on the right hand side. Lean defines subtraction between two natural numbers to be 0 when the result would be negative. That's ok in your case, since descFactorial (n + 1) m would be zero as well. But it's something to look out for when writing your proof. Good luck!

Thanks!

[tsuki hao]

Yongyi Chen said:

One weird thing I noticed is that the variable $k$ and the hypotheses $k\le n$ and $m\le k$ are useless because the $k$ inside the sum is a different variable from the $k$ outside the sum.

Yesss!