summable proving

Stream: new members

[yulia wang]

import mathlib

open Nat Real BigOperators Finset MeasureTheory

namespace intervalIntegral

lemma summable_choose_mul_n_mul_x_pow (k : ℕ) (x : ℝ) (h₀ : x ≥ 0 ∧ x < 1) : Summable fun n => ((Nat.choose n k):ℝ) * n * x ^ n := by

I have some difficulty in proving a function is summable.I am asking for help about the question.

[Weiyi Wang]

How would you prove this on paper? Describing it can help us to find the most intuitive library theorems for you

[Weiyi Wang]

I would probably go with ratio test with https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecificLimits/Normed.html#summable_of_ratio_test_tendsto_lt_one

[yulia wang]

I tried to use Mathematical induction to prove the lemma, but during the proving. I found its too hard. So I want to ask for another way to prove it. My initial code is as follows：

import mathlib

open Nat Real BigOperators Finset MeasureTheory

namespace intervalIntegral

lemma choose_succ_eq_choose (n k: ℕ) (h₀ : n ≥ k): (Nat.choose n (k+1) :ℝ) = Nat.choose n k * ((n-k)/(k+1)):= by
  rw[← mul_left_inj' (c := ((k+1):ℝ))]
  · conv_rhs => rw[mul_assoc]; enter[2];rw[mul_comm, mul_div_assoc']; enter[2]; rw[← mul_one (a:=((k+1):ℝ))]
    rw[mul_div_mul_left,div_one]
    · rw[show ((n-k):ℝ) = (↑(n-k):ℝ) by norm_cast]
      norm_cast
      rw[Nat.choose_succ_right_eq]
    · norm_cast
  · norm_cast

lemma summable_choose_mul_n_mul_x_pow (k : ℕ) (x : ℝ) (h₀ : x ≥ 0 ∧ x < 1) : Summable fun n => ((Nat.choose n k):ℝ) * n * x ^ n := by
      induction k with
      | zero =>
        simp
        refine abs_lt.mpr ?_
        constructor
        · linarith
        · exact h₀.2
      | succ k hk =>
        conv_rhs => ext n; rw[choose_succ_eq_choose]
        sorry

[Eric Wieser]

Your code has an error on the first line; how did you write the rest of the proof despite that?

[Ruben Van de Velde]

Maybe a case-insensitive file system

[yulia wang]

import Mathlib

open Nat Real BigOperators Finset MeasureTheory

namespace intervalIntegral

lemma choose_succ_eq_choose (n k: ℕ) (h₀ : n ≥ k): (Nat.choose n (k+1) :ℝ) = Nat.choose n k * ((n-k)/(k+1)):= by
  rw[← mul_left_inj' (c := ((k+1):ℝ))]
  · conv_rhs => rw[mul_assoc]; enter[2];rw[mul_comm, mul_div_assoc']; enter[2]; rw[← mul_one (a:=((k+1):ℝ))]
    rw[mul_div_mul_left,div_one]
    · rw[show ((n-k):ℝ) = (↑(n-k):ℝ) by norm_cast]
      norm_cast
      rw[Nat.choose_succ_right_eq]
    · norm_cast
  · norm_cast

lemma summable_choose_mul_n_mul_x_pow (k : ℕ) (x : ℝ) (h₀ : x ≥ 0 ∧ x < 1) : Summable fun n => ((Nat.choose n k):ℝ) * n * x ^ n := by
      induction k with
      | zero =>
        simp
        refine abs_lt.mpr ?_
        constructor
        · linarith
        · exact h₀.2
      | succ k hk =>
        conv_rhs => ext n; rw[choose_succ_eq_choose]
        sorry

thanks, M should be capitalized. I don't know why there are no errors on my editor

[Kevin Buzzard]

I would have thought that instead of the hypothesis 0<=x<1 you should have the more general |x|<1

[yulia wang]

The condition for this question to be valid is |x|<1. This is a part of my proving. The title of the entire theorem is

theorem idt (k : ℕ) (x : ℝ) (h₀ : x ≥ 0 ∧ x < 1) (h₁ : k > 0):
  ∑' n : Set.Ici k, (Nat.choose n k) * n ^ 2  * x ^ (n:ℕ) =
  (k ^ 2 + 3 * k * x + x + x ^ 2) * x ^ k / (1 - x) ^ (k + 3) := by

[Kevin Buzzard]

Yes, but your theorem as it stands will not apply for $x=-0.37$ whereas the conclusion is still true (assuming it's true for $0\leq x<1$).

[yulia wang]

You're right. I have reconsidered the proof process. It seems that the theorem will be correct when | x |<1