How to split the sum into two parts

Stream: new members

[tsuki hao]

How to divide \sum k in Icc 0 n, xxx into \sum k in Icc 0 m-1, xxx + \sum k in Icc m n, xxx

[Kevin Buzzard]

What are the types? Can you write a #mwe ?

[tsuki hao]

import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic
import Mathlib.Algebra.BigOperators.Basic

open Nat

open Finset

open BigOperators

theorem idt4 (n : ℕ) : (∑ m in range (n + 1), choose n m) = 2 ^ n := by
  have := (add_pow 1 1 n).symm
  simpa [one_add_one_eq_two] using this

theorem idt6_Absorption_Idt {n k : ℕ} (hkn : k ≤ n) (hsk : 1 ≤ k) :
    k * choose n k  = n * choose (n - 1) (k - 1) := by
      have choose_mul_eq_choose_mul :  choose k 1  * choose n k= choose n 1 * choose (n - 1) (k - 1)  := by rw[mul_comm, choose_mul hkn hsk]
      rw[choose_one_right, choose_one_right] at choose_mul_eq_choose_mul
      rw[choose_mul_eq_choose_mul]


example{n k m : ℕ} (hk : k ≤ n) (hm : m ≤ n) (hkm : m ≤ k) : (∑ 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(k:ℕ) : (choose n k) * (descFactorial (k + 1) m) = (descFactorial (n + 1) m) * choose (n - m) (k - m) := by
 sorry
refine' sum_congr _ fun y _ => h2 (y)

theorem Idt36 {n k m : ℕ } (h1: k ≤ n) (h2 : 1 ≤ k - m): (∑ k in Icc 0 n,  (choose n k) * (descFactorial k m)) = (descFactorial n m) * 2 ^(n - m):= by
  have h0 : (∑ k in Icc 0 n,  (choose n k) * (descFactorial k m)) = (∑ k in Icc 0 n, (descFactorial n m) * choose (n - m) (k - m)) := by
    have h2 (k : ℕ): (choose n k) * (descFactorial k m) = (descFactorial n m) * choose (n - m) (k - m) := by
      induction' m with m ih
      · simp
      · have d1 : descFactorial k (succ m) = (k - m) * (descFactorial k m ) := by
          apply descFactorial_succ
        have d2 : descFactorial n (succ m) = (n - m) * descFactorial n m := by
          apply descFactorial_succ
        have ih2 : descFactorial k m * Nat.choose n k =  Nat.choose n k * descFactorial k m := by
          exact Nat.mul_comm (descFactorial k m) (Nat.choose n k)
        rw[d1]
        rw[d2]
        rw[mul_comm]
        rw[mul_assoc , mul_comm]
        rw[ih2]
        rw[ih]
        have d3 : (k - m) * Nat.choose (n - m) (k - m) = (n - m) * Nat.choose (n - succ m) (k - succ m) := by
          apply idt6_Absorption_Idt
          · have l1 : k ≤ n := by
              sorry
            exact Nat.sub_le_sub_right l1 m
          · sorry
    refine' sum_congr _ fun y _ => h2 (y)
    rfl
  have h1 : (∑ k in Icc 0 n,  (choose n k) * (descFactorial k m)) = (∑ k in Icc m n, (descFactorial n m) * choose (n - m) (k - m)) := by
    have s1 : (∑ k in Icc 0 n,  (choose n k) * (descFactorial k m)) = (∑ k in Icc 0 (m - 1),  (choose n k) * (descFactorial k m)) + (∑ k in Icc m n,  (choose n k) * (descFactorial k m)) := by
      sorry
    have s2 : (∑ k in Icc 0 (m - 1),  (choose n k) * (descFactorial k m)) = 0 := by
      sorry
    rw[s1]
    rw[s2]
    simp

  rw[h1]
  have h3 : (∑ k in Icc m n, descFactorial n m * Nat.choose (n - m) (k - m)) = descFactorial k 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
    simp
    have d1 : (∑ k in Icc m n, Nat.choose (n - m) (k - m)) = (∑ k in range (n - m), Nat.choose n k) := by
      sorry
    rw[d1]
    sorry
  rw[h4]

This corresponds to the third sorry

[Jeremy Tan]

It's docs#Finset.sum_Ico_consecutive. (Icc m n is defeq to Ico m (n + 1))

[Michael Stoll]

You could also look at docs#Finset.sum_Ico_eq_sub .