type class instance error

Stream: maths

[Ashvni Narayanan]

I am trying to state that, te^{Xt} / (e^t - 1) = \sum_{n=1}^{\infty} B_n(X) * t^n / n!, where B_n(X) are Bernoulli polynomials.

import number_theory.bernoulli
import data.nat.basic
import analysis.complex.roots_of_unity
import data.complex.exponential

noncomputable theory
def bernoulli_polynomial (n : ℕ) : ℂ → ℂ := λ X, ∑' i : fin (n+1), (bernoulli n)*(nat.choose n i)*(X^(n-i))

lemma one_sub_eq_neg : ∀ n : ℕ, ∀ X : ℂ, bernoulli_polynomial n (1 - X) = (-1)^n * bernoulli_polynomial n X :=
begin
  sorry
end

lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, ∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i) = (t * real.exp (X * t))/(real.exp t - 1) :=
begin
  sorry
end

I get the error

failed to synthesize type class instance for
t X : ℕ
⊢ add_comm_monoid Prop

I don't see where the add_comm_monoid condition is needed.

Thank you for your help!

[Reid Barton]

I think you must have the wrong $\Sigma$

[Ashvni Narayanan]

Putting ∑ instead of ∑' gives me an error :

unexpected token

[Reid Barton]

Ah, I think there is some open_locale needed maybe?

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

[Yakov Pechersky]

open_locale big_operators?

[Ashvni Narayanan]

Yakov Pechersky said:

open_locale big_operators?

Adding this gives me an error

failed to synthesize type class instance for
t X : ℕ
⊢ fintype ℕ

since, I think, ∑ is for finite sums. Putting ∑' gives me the original error.

[Shing Tak Lam]

I think you're missing some brackets, if you add brackets around the sum it works

lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, (∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i)) = (t * real.exp (X * t))/(real.exp t - 1) :=
begin
  sorry
end

it works

[Ashvni Narayanan]

Shing Tak Lam said:

I think you're missing some brackets, if you add brackets around the sum it works

lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, (∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i)) = (t * real.exp (X * t))/(real.exp t - 1) :=
begin
  sorry
end

it works

Yeah, that works. Why are the brackets needed though?

[Yakov Pechersky]

Because the sum operator is higher different precedence than the =, such that it sums over the whole equality proposition term

[Ashvni Narayanan]

I see. Thank you!