## Stream: maths

### Topic: tsum

#### 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!

#### 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


#### Reid Barton (Dec 03 2020 at 19:41):

ℂ isn't a canonically ordered monoid for a couple reasons

#### Ashvni Narayanan (Dec 04 2020 at 04:47):

Ah, I see now. Thank you!

Last updated: May 10 2021 at 08:14 UTC