has_deriv_at for series

Stream: new members

[Benjamin Davidson]

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]

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]

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

[Dan Stanescu]

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]

I hope I'm wrong about the bug part.

[Alex J. Best]

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]

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