## Stream: new members

### Topic: Using derivative composition

#### Icaro Costa (Jan 11 2023 at 16:56):

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 (Jan 11 2023 at 17:06):

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 (Jan 11 2023 at 17:34):

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ä (Jan 11 2023 at 17:55):

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 (Jan 11 2023 at 18:19):

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 (Jan 11 2023 at 19:05):

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 (Jan 11 2023 at 20:01):

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 (Jan 12 2023 at 01:32):

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 (Jan 12 2023 at 01:34):

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 (Jan 12 2023 at 03:30):

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 (Jan 12 2023 at 12:56):

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 (Jan 12 2023 at 13:01):

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

#### Icaro Costa (Jan 12 2023 at 13:35):

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 (Jan 12 2023 at 13:40):

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 (Jan 12 2023 at 13:55):

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 (Jan 12 2023 at 14:22):

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


Last updated: Dec 20 2023 at 11:08 UTC