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 ff and uu. 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 ff and uu. 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