Nth derivative of a function

Stream: new members

[Icaro Costa]

I want to write a definition Dn that represents the nth derivative in one variable. This is what I'm trying:

import analysis.calculus.deriv
import data.real.basic

/-Function definitions-/
variable (f : ℝ -> ℝ)

noncomputable def D : (ℝ → ℝ) → (ℝ → ℝ)
  | a := deriv a

noncomputable def Dn : ℕ × (ℝ → ℝ) → (ℝ → ℝ)
  | (0, a) := a
  | (1, a) := D a
  | (n+1, a) := Dn (n, a)

I get the error:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (ℕ × (ℝ → ℝ))
    (@prod.has_well_founded ℕ (ℝ → ℝ) (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
       (@has_well_founded_of_has_sizeof (ℝ → ℝ) (default_has_sizeof (ℝ → ℝ))))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
state:
Dn : ℕ × (ℝ → ℝ) → ℝ → ℝ,
n : ℕ,
a : ℝ → ℝ
⊢ prod.lex has_lt.lt (λ (a₁ a₂ : ℝ → ℝ), false) (n, a) (n + 1, a)

I don't understand this error, what does using_well_founded means?

[Sky Wilshaw]

Your function currently takes an argument of type ℕ × (ℝ → ℝ). I'd recommend switching this to a curried function style, where your function type is ℕ → (ℝ → ℝ) → (ℝ → ℝ).

[Sky Wilshaw]

Then I believe the error will disappear.

[Sky Wilshaw]

Are you familiar with functional programming in other languages?

[Yaël Dillies]

You will find docs#nat.iterate useful

[Icaro Costa]

Sky Wilshaw said:

Are you familiar with functional programming in other languages?

This is my first time working with this sort of language

[Sky Wilshaw]

I'd recommend looking at this page in Functional Programming in Lean for more information, but basically:

[Sky Wilshaw]

Suppose your function takes multiple inputs, say, a and b, and outputs c. It's usually easier to define it as a function which takes an input a and spits out a second function, which takes an input b and outputs c.

[Sky Wilshaw]

So you'd write the type as a -> (b -> c), or more concisely, a -> b -> c.

[Sky Wilshaw]

All of Lean's syntax is built to accommodate this programming style, including things like function applications, where you just write f a b instead of f(a)(b).

[Sky Wilshaw]

To answer your original question, Lean will check every definition you write to make sure that it doesn't infinitely loop. The in-built method for determining this wasn't able to verify that Dn doesn't infinitely loop, because it used the comparatively more complicated type ℕ × (ℝ → ℝ). If instead you use just ℕ, then pass (ℝ → ℝ) as another parameter afterwards, it's easier to figure out that it doesn't infinitely loop.

[Sky Wilshaw]

using_well_founded is a way to basically tell Lean a proof that your function doesn't loop infinitely.

[Icaro Costa]

Sky Wilshaw said:

To answer your original question, Lean will check every definition you write to make sure that it doesn't infinitely loop. The in-built method for determining this wasn't able to verify that Dn doesn't infinitely loop, because it used the comparatively more complicated type ℕ × (ℝ → ℝ). If instead you use just ℕ, then pass (ℝ → ℝ) as another parameter afterwards, it's easier to figure out that it doesn't infinitely loop.

Using your explanation, I managed to write this instead:

def Dn : (ℕ) → (ℝ → ℝ) → (ℝ → ℝ)
  | 0 := id
  | 1 := D
  | a := Dn a-1

The last error is gone, but now I receive a message saying "rec_fn_macro only allowed in meta definitions". What is that?

[Mario Carneiro]

that's an error reporting bug, but that definition is not even well founded, it loops infinitely for n >= 2

[Mario Carneiro]

you most likely wanted to write Dn (a-1) instead of Dn a - 1, but this won't work either, because we can't prove in that context that a is nonzero. You can write it with a +1 instead though:

def Dn : (ℕ) → (ℝ → ℝ) → (ℝ → ℝ)
  | 0 := id
  | 1 := D
  | (a+1) := Dn a

[Icaro Costa]

Mario Carneiro said:

you most likely wanted to write Dn (a-1) instead of Dn a - 1, but this won't work either, because we can't prove in that context that a is nonzero. You can write it with a +1 instead though:

def Dn : (ℕ) → (ℝ → ℝ) → (ℝ → ℝ)
  | 0 := id
  | 1 := D
  | (a+1) := Dn a

Somehow it still yields the same error

[Mario Carneiro]

I think the error message is about a missing noncomputable

[Mario Carneiro]

most likely D is a noncomputable def

[Icaro Costa]

Huh, that seems to have worked. What does the noncomputable does exactly?

[Icaro Costa]

Is it that I cannot get a number from it from #eval?

[Mario Carneiro]

it says that lean shouldn't attempt to compile it so you can't use it in #eval

[Icaro Costa]

Ah got it. Thanks!

[Sky Wilshaw]

Note that Dn is not actually the right definition, you probably want D \circ Dn a or something in the (a+1) case.

[Junyan Xu]

You can simply write

import analysis.calculus.deriv
noncomputable def Dn (n : ℕ) (f : ℝ → ℝ) : ℝ → ℝ := deriv^[n] f

F^[n] is notation for docs#nat.iterate

[Mark Andrew Gerads]

iterated_deriv might be what is wanted here.
https://leanprover-community.github.io/mathlib_docs/analysis/calculus/iterated_deriv.html#iterated_deriv