Zulip Chat Archive

Stream: maths

Topic: tsum


view this post on Zulip Ashvni Narayanan (Dec 03 2020 at 18:55):

I am trying to prove a property of Bernoulli polynomials, for which I need to use the lemma tsum_eq_zero_iff. However, I end up with some strange error every time I try to use it :

import number_theory.bernoulli
import data.nat.basic
import analysis.complex.roots_of_unity
import data.complex.exponential
import topology.algebra.infinite_sum

noncomputable theory
open_locale big_operators

class ber (bernoulli_polynomial :     ) :=
(ber :   t : ,  X : , (∑' i : , ((bernoulli_polynomial i X) : ) * t^i / (nat.factorial i)) = (t * complex.exp (X * t)/(complex.exp t - 1) ) )

namespace bernoulli_polynomial

variables (B :     ) [ber B]
--def bernoulli_polynomial (n : ℕ) : ℂ → ℂ := λ X, ∑' i : fin (n+1), (bernoulli n)*(nat.choose n i)*(X^(n-i))
--def bernoulli_polynomial (n : ℕ) : ℂ → ℂ := B n

lemma exp_bernoulli_poly :  t : ,  X : , (∑' i : , (B i X) * t^i / (nat.factorial i)) = (t * complex.exp (X * t)/(complex.exp t - 1) ) :=
ber.ber

lemma exp_bernoulli :  t : , (∑' i : , ((bernoulli i) : ) * t^i / (nat.factorial i)) = (t/(complex.exp t - 1) ) :=
sorry

lemma bernoulli_polynomial_eq_sum (n : ) (X : ) : B n X = ∑' i : fin (n+1), (bernoulli n)*(nat.choose n i)*(X^(n-i)) :=
begin
  sorry
end

lemma one_sub_eq_neg :  n : ,  X : , (B n) ((1: ) - X) = (-1)^n * B n X :=
begin
  rintros n X,
  have h := exp_bernoulli_poly B 1 (1 - X),
  simp at h,
  have h' := exp_bernoulli_poly B (-1) X,
  simp at h',
  have f : complex.exp (1 - X) / (complex.exp 1 - 1) = -complex.exp (-X) / (complex.exp (-1) - 1),
  sorry,
  rw f at h,
  rw <-h' at h,
  rw <-sub_eq_zero_iff_eq at h,
  rw <-tsum_sub at h,
  let g :    := λ b, (B b (1 - X) / (b.factorial) - B b X * (-1) ^ b / (b.factorial)),
  have g' : (∑' b, g b) = 0,
  exact h,
  have g'' : summable g,
  sorry,
  have f' := tsum_eq_zero_iff g'' g',
  sorry
end

The second last line gives me a deterministic timeout.

Any help is appreciated, thank you!

view this post on Zulip Shing Tak Lam (Dec 03 2020 at 19:26):

lemma one_sub_eq_neg :  n : ,  X : , (B n) ((1: ) - X) = (-1)^n * B n X :=
begin
  rintros n X,
  let g :    := λ b, (B b (1 - X) / (b.factorial) - B b X * (-1) ^ b / (b.factorial)),
  have g' : (∑' b, g b) = 0,
  sorry,
  have g'' : summable g,
  sorry,
  have f' := @tsum_eq_zero_iff _ _ _ _ _ g, -- it's failing to find `canonically_ordered_add_monoid ℂ` here
  sorry
end

view this post on Zulip Reid Barton (Dec 03 2020 at 19:41):

isn't a canonically ordered monoid for a couple reasons

view this post on Zulip Ashvni Narayanan (Dec 04 2020 at 04:47):

Ah, I see now. Thank you!


Last updated: May 10 2021 at 08:14 UTC