I have got the proof in informal one.Try to prove it in lean

Stream: new members

[Jasin Jiang]

image.png

import Mathlib

open Nat BigOperators Finset
open Real


theorem idt_120' (n : ℕ) : ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose (n + 1) k -
  ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ (k + 1) / choose (n + 1) (k + 1) = 1 + (-1) ^ n := by
  sorry


theorem idt_120 (n : ℕ) :
  ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose n k = (n + 1) / (n + 2) * (1 + (-1) ^ n) := by
  have h₁ : ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose n k = ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose n k * 1 := by
    simp
  rw [h₁]
  -- have h₂ : ∀ k, k ≤ n → ((n - k + 1) + (k + 1)) / (n + 2) = 1 := by
    -- intro k hk
    -- rw [add_comm, ← add_assoc]
    -- rw [← Nat.add_sub_assoc hk]
    -- rw [add_comm k 1]
    -- have h₂₂ : 1 + k + n - k + 1 = n + 2 := by
    --   simp
    --   symm
    --   rw [add_comm]
    --   omega
    -- rw [h₂₂]
    -- simp
  have h₂ : ∀ k, k ≤ n → ((n - k + 1) + (k + 1)) / (n + 2) = (1 : ℝ) := by
    intro k hk
    field_simp
    linarith
  simp_rw [← Ring.choose_natCast]

So painful. Who can give me some advice?

[Ruben Van de Velde]

Okay, then the next step is to write the statement in lean. Have you done that?

[Jasin Jiang]

I don't know how to continue writing

import Mathlib

open Nat BigOperators Finset
open Real


theorem idt_120' (n : ℕ) : ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose (n + 1) k -
  ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ (k + 1) / choose (n + 1) (k + 1) = 1 + (-1) ^ n := by
  sorry


theorem idt_120 (n : ℕ) :
  ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose n k = (n + 1) / (n + 2) * (1 + (-1) ^ n) := by

  have h₁ : ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose n k
    = ∑ k in Finset.range (n + 1), 1 * (-1 : ℝ) ^ k / choose n k := by
    simp
  rw [h₁]
  have h₂ : ∑ k in Finset.range (n + 1), 1 * (-1 : ℝ) ^ k / choose n k
    = ∑ k in Finset.range (n + 1), (n + 2) / (n + 2) * (-1 : ℝ) ^ k / choose n k := by
    field_simp
  rw [h₂]
  have h₃ : ∑ k in Finset.range (n + 1), (n + 2) / (n + 2) * (-1 : ℝ) ^ k / choose n k =
    (1 : ℝ) / (n + 2) * ∑ k in Finset.range (n + 1), (n + 2) * (-1 : ℝ) ^ k / choose n k := by
    rw [← sum_mul (1 : ℝ / (n + 2))]



















  -- -- have h₂ : ∀ k, k ≤ n → ((n - k + 1) + (k + 1)) / (n + 2) = 1 := by
  --   -- intro k hk
  --   -- rw [add_comm, ← add_assoc]
  --   -- rw [← Nat.add_sub_assoc hk]
  --   -- rw [add_comm k 1]
  --   -- have h₂₂ : 1 + k + n - k + 1 = n + 2 := by
  --   --   simp
  --   --   symm
  --   --   rw [add_comm]
  --   --   omega
  --   -- rw [h₂₂]
  --   -- simp
  -- have h₂ : ∀ k, k ≤ n → ((n - k + 1) + (k + 1)) / (n + 2) = (1 : ℝ) := by
  --   intro k hk
  --   field_simp
  --   linarith

Ruben Van de Velde said:

Okay, then the next step is to write the statement in lean. Have you done that?

[Ruben Van de Velde]

That's good. Lean is getting confused by a number of things here. First, the syntax for type ascription includes the parentheses, so (1 : ℝ / (n + 2)) needs to be ((1 : ℝ) / (n + 2)). Second, it turns out that sum_mul has more explicit arguments before the constant, so you need to write sum_mul _ _ ((1 : ℝ) / (n + 2)). Third, your multiplication has the constant on the left, not the right, so write mul_sum _ _ ((1 : ℝ) / (n + 2)) instead. And fourth, you don't quite have the sum in the right shape yet for mul_sum to work either. You can go the other direction and drop the ←. Then you just need to do a final bit of arithmetic under the sum to finish h₃

[Jasin Jiang]

Ruben Van de Velde said:

That's good. Lean is getting confused by a number of things here. First, the syntax for type ascription includes the parentheses, so (1 : ℝ / (n + 2)) needs to be ((1 : ℝ) / (n + 2)). Second, it turns out that sum_mul has more explicit arguments before the constant, so you need to write sum_mul _ _ ((1 : ℝ) / (n + 2)). Third, your multiplication has the constant on the left, not the right, so write mul_sum _ _ ((1 : ℝ) / (n + 2)) instead. And fourth, you don't quite have the sum in the right shape yet for mul_sum to work either. You can go the other direction and drop the ←. Then you just need to do a final bit of arithmetic under the sum to finish h₃

thank you so much. If I have another question I will ask for some help again!

[Jasin Jiang]

theorem idt_120' (n : ℕ) : ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ k / choose (n + 1) k -
  ∑ k in Finset.range (n + 1), (-1 : ℝ) ^ (k + 1) / choose (n + 1) (k + 1) = 1 + (-1) ^ n := by
  sorry

one question left. How to prove this?

[Jasin Jiang]

I want to use induction, but it seems to be not correct

[Ruben Van de Velde]

Why? The calculation you posted at the top of the thread does not use induction

[Jasin Jiang]

Ruben Van de Velde said:

Why? The calculation you posted at the top of the thread does not use induction

Since I am using mathematical induction, the binomial coefficient in the denominator, , will change to , which I feel is not easy to handle for induction.

[Jasin Jiang]

do you have some ideas for solving this problem in Lean4?

[Ruben Van de Velde]

No, I'm asking why you're using induction at all for this problem

[Jasin Jiang]

ok~

[Mitchell Lee]

If you haven't already, I highly recommend that you read this: https://www2.math.upenn.edu/~wilf/AeqB.html

[Mitchell Lee]

The algorithms in this book have not been implemented in mathlib as far as I am aware, but they can in principle handle binomial coefficient sums like the ones you have been asking about.

[Notification Bot]

This topic was moved here from #general > I have got the proof in informal one.Try to prove it in lean by Yury G. Kudryashov.