Derivative

Stream: general

[Icaro Costa]

How do I import the derivative operator D. The one from import analysis.calculus.deriv doesn't seem to work with "powers" and it seems to require the function to be evaluated at some point. I would like to have D as a linear operator acting on the vector space of real differentiable functions and have powers of D to represent its nth-order derivatives.

Basically, I want to set up a space where I can do this:

$D(\alpha f + g) = \alpha D f + Dg$

And

$D^2 f = D (D f)$

Notice that I am not evaluating any of these functions at some $x \in \mathbb{R}$.

Is there a package that already does this in Lean3?

[Moritz Doll]

docs#iterated_deriv and docs#iterated_deriv_eq_iterate

[Icaro Costa]

I am trying to define D on top of deriv now. This is an attempt to prove the product rule for D based on deriv.

noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f
noncomputable variable x : ℝ

lemma product_rule (h g : ℝ → ℝ)(hIsDiff : differentiable ℝ h)(gIsDiff : differentiable ℝ g):
  D (h • g) = h • D g + g • D h :=
begin
  unfold D,
  ext x,
  apply deriv_smul (hIsDiff x) (gIsDiff x),
end

The error I receive is

invalid apply tactic, failed to unify
  deriv (h • g) x = (h • deriv g + g • deriv h) x
with
  deriv (λ (y : ℝ), h y • g y) x = h x • deriv g x + deriv h x • g x
state:
h g : ℝ → ℝ,
hIsDiff : differentiable ℝ h,
gIsDiff : differentiable ℝ g,
x : ℝ
⊢ deriv (h • g) x = (h • deriv g + g • deriv h) x

Isn't the lambda expression exactly what I have on the left side? What is the right way to implement this?

[Kevin Buzzard]

Why are you defining D when it's definitionally equal to deriv? Or did I miss something?

You haven't posted a #mwe so I'm not in a position to diagnose your error. Is h x • g x definitionally equal to (h • g) x and similar for the right hand side? If not then that's your problem. If it is then try using refine (and adding in the appropriate holes) instead of apply, apply is occasionally flaky because of the apply bug.

[Icaro Costa]

Kevin Buzzard said:

Why are you defining D when it's definitionally equal to deriv? Or did I miss something?

You haven't posted a #mwe so I'm not in a position to diagnose your error. Is h x • g x definitionally equal to (h • g) x and similar for the right hand side? If not then that's your problem. If it is then try using refine (and adding in the appropriate holes) instead of apply, apply is occasionally flaky because of the apply bug.

The reason I am defining this D is both for convenience and for me to learn the syntax and how to work out the proofs.

I suppose this should serve as an mwe:

import data.real.basic
import data.list.basic
import tactic
import algebra.big_operators.basic
import data.nat.interval
import data.vector
import data.nat.basic
import analysis.calculus.deriv
import algebra.group.defs

open_locale big_operators
open finset

-- Definition of the derivative operator and its properties
noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f

noncomputable variable x : ℝ

lemma product_rule (h g : ℝ → ℝ)(hIsDiff : differentiable ℝ h)(gIsDiff : differentiable ℝ g):
  D (h • g) = h • D g + g • D h :=
begin
  unfold D,
  ext x,
  apply deriv_smul (hIsDiff x) (gIsDiff x),
end

Answering your other question, yes. h x • g x should be equal to (h • g) x, but I don't think Lean got that.

[Kevin Buzzard]

The right hand sides are not definitionally equal though:

lemma product_rule (h g : ℝ → ℝ)(hIsDiff : differentiable ℝ h)(gIsDiff : differentiable ℝ g):
  D (h • g) = h • D g + g • D h :=
begin
  unfold D,
  ext x,
  convert deriv_smul (hIsDiff x) (gIsDiff x),
  -- ⊢ (h • deriv g + g • deriv h) x = h x • deriv g x + deriv h x • g x
end

You need to commute g and deriv h; that's the reason it won't unify. Lean did get that the left hand sides were definitionally equal (that's why we don't see the left hand side as a goal produced by convert)

[Kevin Buzzard]

-- I changed the statement of the lemma to be more mathlib-like
lemma product_rule (h g : ℝ → ℝ)(hIsDiff : differentiable ℝ h)(gIsDiff : differentiable ℝ g):
  D (h • g) = h • D g + D h • g :=
begin
  unfold D,
  ext x,
  exact deriv_smul (hIsDiff x) (gIsDiff x), -- `exact` is better than `apply`, which only
  -- works due to a coincidence basically
end

[Kevin Buzzard]

tl;dr:

Isn't the lambda expression exactly what I have on the left side?

No ;-) (but I only spotted this once I had working code in front of me, that's the joys of a mwe)

[Icaro Costa]

Kevin Buzzard said:

-- I changed the statement of the lemma to be more mathlib-like
lemma product_rule (h g : ℝ → ℝ)(hIsDiff : differentiable ℝ h)(gIsDiff : differentiable ℝ g):
  D (h • g) = h • D g + D h • g :=
begin
  unfold D,
  ext x,
  exact deriv_smul (hIsDiff x) (gIsDiff x), -- `exact` is better than `apply`, which only
  -- works due to a coincidence basically
end

I haven't seen this keyword convert yet, but it seems to do exactly what I was trying to accomplish. What I noticed is that if swap D h • g by g • D h in the lemma proposition, the proof doesn't work anymore. Is this because I would also have to prove that • commutes in this context?

Does the keyword convert "applies" the lambda function onto x before trying to replace it?

Thank you for your help btw

[Kevin Buzzard]

apply is just doing exact and exact doesn't work because it's not exactly right. convert h is just exact h except it gives the user back the parts of the goal which weren't exactly h