Using derivative composition

Stream: new members

[Icaro Costa]

Code:

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

import algebra.group.defs

open_locale big_operators

open finset

/-Function definitions-/
variable (f : ℝ → ℝ)
variable (u : ℝ → ℝ)


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

/-Higher order derivatives-/
noncomputable def Dn : (ℕ) → (ℝ → ℝ) → (ℝ → ℝ)
  | 0 := λ f, id ∘ f
  | 1 := λ f, D f
  | (a+1) := λ f, Dn a (D f)

/-Derivative rules-/
def product_rule := D f*u = (D f)*u + f*(D u)

def composite_deriv := D (f ∘ u) = (D f) ∘ u + f ∘ (D u)

/-Composite function derivative-/
lemma second_composite_deriv (x: ℝ) : Dn 2 (f ∘ u) x = (((D (D f)) ∘ u)*(D u)^2 + ((D f) ∘ u)*(D (D u))) x :=
begin
  unfold Dn, /-Out: D (D (f ∘ u)) x = (D (D f) ∘ u * D u ^ 2 + D f ∘ u * D (D u)) x-/
  rw composite_deriv f u,
end

Problem:

Using rw composite_deriv f u fails with message: "rewrite tactic failed, lemma is not an equality nor a iff". Why is it giving me this error? Isn't my lemma already an equality?

[Icaro Costa]

It also doesn't seem to work with the "obvious" case, it yields the same error message.

/-Composite function with first derivative-/
lemma first_composite_deriv : Dn 1 (f ∘ u) = (D f) ∘ u + f ∘ (D u) :=
begin
  unfold Dn,
  rw composite_deriv f u,
end

[Icaro Costa]

It seems to be a problem with the definition of Dn again:

/-Higher order derivatives-/
def Dn: ℕ → ((ℝ → ℝ) → (ℝ → ℝ))
  | 0 := id
  | (n+1) := D ∘ Dn n

#check Dn 0

The check returns a map Dn 0 : ℕ → (ℝ → ℝ) → ℝ → ℝ, but I would be expecting (ℝ → ℝ) → (ℝ → ℝ), which is just id.

[Kalle Kytölä]

It is a bit unclear what you are trying above. The product_rule and composite_deriv you have defined are statements (about a pair of real functions), not results. You can see this in Lean by, e.g., #check product_rule. This explains why the rewrite fails --- indeed "...lemma is not an equality nor a iff".

The statement product_rule f u would in fact be a true statement if one furthermore assumes differentiability of $f$ and $u$. Under that hypothesis you could therefore make it a result (prove it). The content of it would be more or less docs#deriv_mul.

It is less clear under what reasonable assumptions your composite_deriv would be true. Did you mean something more like the chain rule, docs#deriv.comp?

[Mark Andrew Gerads]

Look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/iterated_deriv.html#iterated_deriv
You do not need to redefine what was already defined.

[Icaro Costa]

Kalle Kytölä said:

It is a bit unclear what you are trying above. The product_rule and composite_deriv you have defined are statements (about a pair of real functions), not results. You can see this in Lean by, e.g., #check product_rule. This explains why the rewrite fails --- indeed "...lemma is not an equality nor a iff".

The statement product_rule f u would in fact be a true statement if one furthermore assumes differentiability of $f$ and $u$. Under that hypothesis you could therefore make it a result (prove it). The content of it would be more or less docs#deriv_mul.

It is less clear under what reasonable assumptions your composite_deriv would be true. Did you mean something more like the chain rule, docs#deriv.comp?

I want to use those as "substitutions" in the proof, that's why I'm calling rewrite. Am I supposed to write this instead?

/-Derivative rules-/
def product_rule D f*u := (D f)*u + f*(D u)

def composite_deriv D (f ∘ u) := (D f) ∘ u + f ∘ (D u)

[Icaro Costa]

Mark Andrew Gerads said:

Look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/iterated_deriv.html#iterated_deriv
You do not need to redefine what was already defined.

The reason I am redefining it is to learn the language by proving things that I already know.

[Sky Wilshaw]

I think what you need to do is actually prove that the product rule holds.

lemma product_rule D f u (and some differentiability hypotheses) : D (f * u) = (D f)*u + f*(D u) :=
begin
...
end

Your current definitions are just that: definitions. They're not proofs of any fact, so you can't use them to rewrite e.g. D (f * u) into (D f) * u + f * (D u).

More precisely, when you write def product_rule := D f*u = (D f)*u + f*(D u), you create a new proposition called product_rule D f u which is true when the product rule holds on f and u, and false when it doesn't hold.

[Sky Wilshaw]

Using your original definitions, you could make a theorem like this:

lemma deriv_eq_of_product_rule : product_rule D f u → D f*u = (D f)*u + f*(D u) :=
begin
  intro h,
  unfold product_rule at h,
  exact h,
end

which says that "when the product rule holds for f and u, we have D f*u = (D f)*u + f*(D u).

[Junyan Xu]

Note D f*u is exactly the same as (D f)*u.
You can also pretend the proposition is true by writing

lemma product_rule : D f*u = (D f)*u + f*(D u) := sorry

or

axiom product_rule : D f*u = (D f)*u + f*(D u)

Icaro Costa said:

It seems to be a problem with the definition of Dn again:

#check Dn 0

The check returns a map Dn 0 : ℕ → (ℝ → ℝ) → ℝ → ℝ, but I would be expecting (ℝ → ℝ) → (ℝ → ℝ), which is just id.

By the way, I can't reproduce this. I get Dn 0 : (ℝ → ℝ) → ℝ → ℝ.

[Icaro Costa]

Junyan Xu said:

Note D f*u is exactly the same as (D f)*u.
You can also pretend the proposition is true by writing

lemma product_rule : D f*u = (D f)*u + f*(D u) := sorry

or

axiom product_rule : D f*u = (D f)*u + f*(D u)

Icaro Costa said:

It seems to be a problem with the definition of Dn again:

#check Dn 0

The check returns a map Dn 0 : ℕ → (ℝ → ℝ) → ℝ → ℝ, but I would be expecting (ℝ → ℝ) → (ℝ → ℝ), which is just id.

By the way, I can't reproduce this. I get Dn 0 : (ℝ → ℝ) → ℝ → ℝ.

Hm that's interesting, I think that an axiom is what I really wanted. However, I am still having problems about the definition of a higher order derivative:

/-Identiy operator-/
def Id : (ℝ → ℝ) → (ℝ → ℝ) := λ x, x

/-Higher order derivatives-/
def Dn: ℕ → ((ℝ → ℝ) → (ℝ → ℝ))
  | 0 := Id
  | (n+1) := D ∘ Dn n

Doing #check Dn 1 outputs a type Dn 1 : ℕ → (ℝ → ℝ) → ℝ → ℝ while what I really want is Dn 1 : (ℝ → ℝ) → (ℝ → ℝ). Any way I can make this work?

[Reid Barton]

Do you have some variables/include lying around? What does #check Dn say?

[Icaro Costa]

Reid Barton said:

Do you have some variables/include lying around? What does #check Dn say?

Doing #check Dn gives me Dn : ((ℝ → ℝ) → ℝ → ℝ) → ℕ → (ℝ → ℝ) → ℝ → ℝ, which doesn't make sense to me.

The variables that I have are these:

/-Function definitions-/
variable (f : ℝ → ℝ)
variable (u : ℝ → ℝ)

/-Derivative-/
variable (D: (ℝ → ℝ) → (ℝ → ℝ))

[Yaël Dillies]

The first argument to Dn is the variable D, not the variable n. So either you write Dn deriv n, or you turn D into a def

[Icaro Costa]

Yaël Dillies said:

The first argument to Dn is the variable D, not the variable n. So either you write Dn deriv n, or you turn D into a def

That fixed it!

[Icaro Costa]

Here's the working code if anyone is interested:

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

import algebra.group.defs

open_locale big_operators

open finset

/-Function definitions-/
def f : ℝ → ℝ := sorry
def u : ℝ → ℝ := sorry

/-Derivative-/
def D: (ℝ → ℝ) → (ℝ → ℝ) := sorry

/-Identiy operator-/
def Id : (ℝ → ℝ) → (ℝ → ℝ) := λ (x : ℝ → ℝ), x

/-Higher order derivatives-/
def Dn: ℕ → ((ℝ → ℝ) → (ℝ → ℝ))
  | 0 := Id
  | (n+1) := D ∘ Dn n

#check Dn 1

/-Derivative rules-/
axiom product_rule (h : ℝ → ℝ)(g : ℝ → ℝ): D (h*g) = (D h)*g + h*(D g)
axiom composite_deriv (h : ℝ → ℝ)(g : ℝ → ℝ): D (h ∘ g) = ((D h) ∘ g) * (D g)

/-Composite function with first derivative-/
lemma first_composite_deriv : (Dn 1) (f ∘ u) = ((D f) ∘ u)*(D u) :=
begin
  unfold Dn,
  simp,
  rw Id,
  simp,
  rw composite_deriv f u,
end

/-Composite function with second derivative-/
lemma second_composite_deriv : Dn 2 (f ∘ u) = (((D (D f)) ∘ u)*(D u)*(D u) + ((D f) ∘ u)*(D (D u))):=
begin
  unfold Dn,
  simp,
  rw Id,
  simp,
  rw composite_deriv f u,
  rw product_rule (D f ∘ u) (D u),
  rw composite_deriv (D f) u,
end