Section Nth_Derivative.

Nth Derivative

We now study higher order differentiability.

Throughout this section:

a, b will be real numbers with a < b;
I will denote the compact interval [a,b];
F, G, H will denote partial functions.

Definitions

We first define what we mean by the derivative of order n of a function.

Variables a b : IR.
Hypothesis Hab' : a[<]b.

Fixpoint Derivative_I_n (n : N) (F Fn : PartIR) {struct n} : CProp :=
  match n with
  | O => ≈ I F Fn
  | S p => {f' : CSetoid_fun (subset (Compact Hab)) IR |
      Derivative_I Hab' F (PartInt f') | Derivative_I_n p (PartInt f') Fn}
  end.

Unlike first order differentiability, for our definition to be workable it is better to define directly what it means for a function to be n times differentiable instead of quantifying over the Derivative_I_n relation.

Fixpoint Diffble_I_n (n : N) (F : PartIR) {struct n} : CProp :=
  match n with
  | O => ⊆ I (Dom F)
  | S p => {H : Diffble_I Hab' F | Diffble_I_n p (PartInt (ProjT1 H))}
  end.

End Nth_Derivative.

Section Trivia.

Trivia

These are the expected extensionality and uniqueness results.

Variables a b : IR.
Hypothesis Hab' : a[<]b.

Lemma Diffble_I_n_wd : forall n F G,
≈ I F G -> Diffble_I_n Hab' n F -> Diffble_I_n Hab' n G.

Lemma Derivative_I_n_wdr : forall n F G H,
≈ I G H -> Derivative_I_n Hab' n F G -> Derivative_I_n Hab' n F H.

Lemma Derivative_I_n_wdl : forall n F G H,
≈ I F G -> Derivative_I_n Hab' n F H -> Derivative_I_n Hab' n G H.

Lemma Derivative_I_n_unique : forall n F G H,
Derivative_I_n Hab' n F G -> Derivative_I_n Hab' n F H -> ≈ I G H.

End Trivia.

Section Basic_Results.

Basic Results

We now explore the concept of n times differentiability. Notice that, unlike the first order case, we do not pay so much attention to the relation of n times derivative, but focus rather on the definition of Diffble_I_n.

Variables a b : IR.
Hypothesis Hab' : a[<]b.

We begin by showing that having a higher order derivative implies being differentiable.

Lemma Diffble_I_n_imp_diffble : forall n : N,
0 < n -> forall F : PartIR, Diffble_I_n Hab' n F -> Diffble_I Hab' F.

Lemma deriv_n_imp_diffble : forall n : N, 0 < n ->
forall F F' : PartIR, Derivative_I_n Hab' n F F' -> Diffble_I Hab' F.

If a function is n times differentiable then it is also m times differentiable for every m less or equal than n.

Lemma le_imp_Diffble_I : forall m n : N, m <= n ->
forall F, Diffble_I_n Hab' n F -> Diffble_I_n Hab' m F.

The next result consolidates our intuition that a function is n times differentiable if we can build from it a chain of n derivatives.

Lemma Diffble_I_imp_le : forall n, 0 < n -> forall F F',
Diffble_I_n Hab' n F -> Derivative_I Hab' F F' -> Diffble_I_n Hab' (pred n) F'.

As expected, an n times differentiable in [a,b] function must be defined in that interval.

Lemma Diffble_I_n_imp_inc : forall n F,
Diffble_I_n Hab' n F -> ⊆ (Compact Hab) (Dom F).

Also, the notions of derivative and differentiability are related as expected.

Lemma Diffble_I_n_imp_deriv_n : forall n F, Diffble_I_n Hab' n F ->
{f' : CSetoid_fun (subset (Compact Hab)) IR | Derivative_I_n Hab' n F (PartInt f')}.

Lemma deriv_n_imp_Diffble_I_n : forall n F F',
Derivative_I_n Hab' n F F' -> Diffble_I_n Hab' n F.

From this we can prove that if F has an nth order derivative in [a,b] then both F and its derivative are defined in that interval.

Lemma Derivative_I_n_imp_inc : forall n F F',
Derivative_I_n Hab' n F F' -> ⊆ I (Dom F).

Lemma Derivative_I_n_imp_inc' : forall n F F',
Derivative_I_n Hab' n F F' -> ⊆ I (Dom F').

Section aux.

First order differentiability is just a special case.

Variable F : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffFn : Diffble_I_n Hab' 1 F.

Lemma deriv_1_deriv : ≈ I
(PartInt (ProjT1 diffF)) (PartInt (ProjT1 (Diffble_I_n_imp_deriv_n _ _ diffFn))).

Lemma deriv_1_deriv' : forall (x : subset I),
ProjT1 diffF x [=] ProjT1 (Diffble_I_n_imp_deriv_n _ _ diffFn) x.

End aux.

As usual, nth order derivability is preserved by shrinking the interval.

Lemma included_imp_deriv_n : forall n c d Hcd F F',
⊆ (Compact (less_leEq _ c d Hcd)) (Compact (less_leEq _ a b Hab')) ->
Derivative_I_n Hab' n F F' -> Derivative_I_n Hcd n F F'.

Lemma included_imp_diffble_n : forall n c d Hcd F,
⊆ (Compact (less_leEq _ c d Hcd)) (Compact (less_leEq _ a b Hab')) ->
Diffble_I_n Hab' n F -> Diffble_I_n Hcd n F.

And finally we have an addition rule for the order of the derivative.

Lemma Derivative_I_n_plus : forall n m k F G H, Derivative_I_n Hab' m F G ->
Derivative_I_n Hab' n G H -> k = m + n -> Derivative_I_n Hab' k F H.

End Basic_Results.

Section More_Results.

Variables a b : IR.
Hypothesis Hab' : a[<]b.

The Nth Derivative

We now define an operator that returns an nth order derivative of an n-times differentiable function. This is analogous to the quantifier elimination which we would get if we had defined nth differentiability as an existential quantification of the nth derivative relation.

Definition n_deriv_I n F (H : Diffble_I_n Hab' n F) : PartIR.

Defined.

This operator is well defined and works as expected.

Lemma n_deriv_I_wd : forall n F G Hf Hg,
≈ I F G -> ≈ I (n_deriv_I n F Hf) (n_deriv_I n G Hg).

Lemma n_deriv_lemma : forall n F H, Derivative_I_n Hab' n F (n_deriv_I n F H).

Lemma n_deriv_inc : forall n F H, ⊆ (Compact Hab) (Dom (n_deriv_I n F H)).

Lemma n_deriv_inc' : forall n Hab F H, ⊆ (Dom (n_deriv_I n F H)) (compact a b Hab).

Some basic properties of this operation.

Lemma n_Sn_deriv : forall n F H HS,
Derivative_I Hab' (n_deriv_I n F H) (n_deriv_I (S n) F HS).
Included.
Included.
Qed.

Lemma n_deriv_plus : forall m n F H H',
Derivative_I_n Hab' m (n_deriv_I n F H) (n_deriv_I (m + n) F H').

End More_Results.

Section More_on_n_deriv.

Some not so basic properties of this operation (needed in rather specific situations).

Lemma n_deriv_I_wd' : forall n a b Hab a' b' Hab' F H H' x y, x [=] y ->
Compact (less_leEq _ _ _ Hab) x -> Compact (less_leEq _ _ _ Hab') y ->
Diffble_I_n (Min_less_Max _ _ a' b' Hab) n F -> forall Hx Hy,
n_deriv_I a b Hab n F H x Hx [=] n_deriv_I a' b' Hab' n F H' y Hy.

Lemma n_deriv_I_wd'' : forall n a b Hab Hab' F H H' x y, x [=] y ->
Compact (less_leEq _ _ _ Hab) x -> Compact (less_leEq _ _ _ Hab) y ->
forall Hx Hy, n_deriv_I a b Hab n F H x Hx [=] n_deriv_I a b Hab' n F H' y Hy.

Lemma n_deriv_I_strext' : forall n a b Hab a' b' Hab' F H H' x y,
Compact (less_leEq _ _ _ Hab) x -> Compact (less_leEq _ _ _ Hab') y ->
Diffble_I_n (Min_less_Max _ _ a' b' Hab) n F -> (forall Hx Hy,
n_deriv_I a b Hab n F H x Hx [#] n_deriv_I a' b' Hab' n F H' y Hy) -> x [#] y.

End More_on_n_deriv.