Zulip Chat Archive

Stream: maths

Topic: type class instance error


view this post on Zulip Ashvni Narayanan (Dec 02 2020 at 16:14):

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!

view this post on Zulip Reid Barton (Dec 02 2020 at 16:15):

I think you must have the wrong Σ\Sigma

view this post on Zulip Ashvni Narayanan (Dec 02 2020 at 16:21):

Putting instead of ∑' gives me an error :

unexpected token

view this post on Zulip Reid Barton (Dec 02 2020 at 16:23):

Ah, I think there is some open_locale needed maybe?

view this post on Zulip Reid Barton (Dec 02 2020 at 16:23):

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

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 16:23):

open_locale big_operators?

view this post on Zulip Ashvni Narayanan (Dec 02 2020 at 16:27):

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.

view this post on Zulip Shing Tak Lam (Dec 02 2020 at 16:30):

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

view this post on Zulip Ashvni Narayanan (Dec 02 2020 at 16:40):

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?

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 16:41):

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

view this post on Zulip Ashvni Narayanan (Dec 02 2020 at 17:29):

I see. Thank you!


Last updated: May 19 2021 at 02:10 UTC