tsum

Stream: maths

[Ashvni Narayanan]

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]

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]

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

[Ashvni Narayanan]

Ah, I see now. Thank you!