Zulip Chat Archive

Stream: new members

Topic: has_deriv_at for series


view this post on Zulip Benjamin Davidson (Jul 24 2020 at 20:46):

I'm having trouble working with has_deriv_at in order to set up hypotheses to use with has_deriv_at.sum. My h1 in the code below gives me a strange error message and I can't figure out how to resolve it. (For comparison, I've included h2, which does not result in that same error.)

import analysis.calculus.deriv

def a (i:)(x:): := x^i
def a' (i:)(x:): := i * x^(i-1)

example (x:) (k:) : 1=2 :=
begin
  have h1 : (2  finset.range k)  (has_deriv_at (a 2) (a' 2 x) x) := by sorry,
  have h2 : (has_deriv_at (a 2) (a' 2 x) x) := by sorry,
end

The error message I get is:

function expected at
  a
term has type
  2  finset.range k

view this post on Zulip Dan Stanescu (Jul 24 2020 at 22:56):

The a-bug? This works.

def b (i:)(x:): := x^i
def a' (i:)(x:): := i * x^(i-1)

example (x:) (k:) : 1=2 :=
begin
  have h1 : (2  finset.range k)  (has_deriv_at (b 2) (a' 2 x) x) := by sorry,
  have h2 : (has_deriv_at (b 2) (a' 2 x) x) := by sorry,
  sorry,
end

view this post on Zulip Heather Macbeth (Jul 24 2020 at 23:11):

By "a bug", do you mean a bug that hits only when you name a variable a? :smiley:

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:13):

I have no idea. It was just a joke, but it does look like a bug and it appears that the name of the variable plays a role.

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:13):

I hope I'm wrong about the bug part.

view this post on Zulip Alex J. Best (Jul 24 2020 at 23:16):

This could be the infamous a bug https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Is.20this.20a.20bug.3F/near/172013398

view this post on Zulip Benjamin Davidson (Jul 24 2020 at 23:27):

Wow. Thanks for the help! Would never have guessed that this was the problem.


Last updated: May 08 2021 at 04:14 UTC