Stream: new members

Topic: has_deriv_at for series

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


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


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:

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.

Dan Stanescu (Jul 24 2020 at 23:13):

I hope I'm wrong about the bug part.

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

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