# Zulip Chat Archive

## 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 atruestatement 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):

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 (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