CoRN.ftc.Differentiability
Differentiability
Definition Diffble_I (a b : IR) (Hab : a [<] b) (F : PartIR) :=
{f' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR |
Derivative_I Hab F (PartInt f')}.
End Definitions.
Implicit Arguments Diffble_I [a b].
Section Local_Properties.
From this point on, we just prove results analogous to the ones for derivability.
A function differentiable in [a,b] is differentiable in every proper compact subinterval of [a,b].
Lemma included_imp_diffble : ∀ a b Hab c d Hcd F,
included (compact c d (less_leEq _ _ _ Hcd)) (compact a b (less_leEq _ _ _ Hab)) →
Diffble_I Hab F → Diffble_I Hcd F.
Proof.
intros a b Hab c d Hcd F H H0.
elim H0; clear H0; intros f' derF.
∃ (IntPartIR (F:=(Frestr (F:=PartInt f') (compact_wd _ _ _) H)) (included_refl _ _)).
apply Derivative_I_wdr with (PartInt f').
FEQ.
simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra.
exact (included_imp_deriv _ _ _ _ _ _ _ _ H derF).
Qed.
A function differentiable in an interval is everywhere defined in that interval.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Lemma diffble_imp_inc : ∀ F, Diffble_I Hab' F → included I (Dom F).
Proof.
intros F H.
inversion_clear H.
unfold I, Hab in |- *; Included.
Qed.
If a function has a derivative in an interval then it is differentiable in that interval.
Lemma deriv_imp_Diffble_I : ∀ F F', Derivative_I Hab' F F' → Diffble_I Hab' F.
Proof.
intros F F' H.
∃ (IntPartIR (derivative_imp_inc' _ _ _ _ _ H)).
apply Derivative_I_wdr with F'.
apply int_part_int.
assumption.
Qed.
End Local_Properties.
Hint Resolve diffble_imp_inc: included.
Section Operations.
All the algebraic results carry on.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Section Constants.
Lemma Diffble_I_const : ∀ c : IR, Diffble_I Hab' [-C-]c.
Proof.
intros.
∃ (IConst (Hab:=Hab) [0]).
apply Derivative_I_wdr with ( [-C-][0]:PartIR).
apply part_int_const.
Deriv.
Qed.
Lemma Diffble_I_id : Diffble_I Hab' FId.
Proof.
∃ (IConst (Hab:=Hab) [1]).
apply Derivative_I_wdr with ( [-C-][1]:PartIR).
apply part_int_const.
Deriv.
Qed.
Lemma Diffble_I_poly : ∀ p, Diffble_I Hab' (FPoly _ p).
Proof.
intros p.
∃ (@IntPartIR (FPoly _ (_D_ p)) _ _ Hab (included_IR _)).
apply Derivative_I_wdr with (FPoly _ (_D_ p)).
apply int_part_int.
Deriv.
Qed.
End Constants.
Section Well_Definedness.
Variables F H : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Lemma Diffble_I_wd : Feq (Compact Hab) F H → Diffble_I Hab' H.
Proof.
intro H0.
∃ (ProjT1 diffF).
eapply Derivative_I_wdl.
apply H0.
apply projT2.
Qed.
End Well_Definedness.
Variables F G : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffG : Diffble_I Hab' G.
Lemma Diffble_I_plus : Diffble_I Hab' (F{+}G).
Proof.
elim diffF; intros F' derF.
elim diffG; intros G' derG.
∃ (IPlus F' G').
eapply Derivative_I_wdr.
apply part_int_plus with (F := PartInt F') (G := PartInt G').
apply Feq_reflexive; Included.
apply Feq_reflexive; Included.
Deriv.
Qed.
Lemma Diffble_I_inv : Diffble_I Hab' {--}F.
Proof.
elim diffF; intros F' derF.
∃ (IInv F').
eapply Derivative_I_wdr.
apply part_int_inv with (F := PartInt F').
apply Feq_reflexive; Included.
Deriv.
Qed.
Lemma Diffble_I_mult : Diffble_I Hab' (F{*}G).
Proof.
elim diffF; intros F' derF.
elim diffG; intros G' derG.
∃ (IPlus (IMult (IntPartIR (diffble_imp_inc _ _ _ _ diffF)) G')
(IMult F' (IntPartIR (diffble_imp_inc _ _ _ _ diffG)))).
eapply Derivative_I_wdr.
apply part_int_plus with (F := PartInt (IMult (IntPartIR (diffble_imp_inc _ _ _ _ diffF)) G'))
(G := PartInt (IMult F' (IntPartIR (diffble_imp_inc _ _ _ _ diffG)))).
apply Feq_reflexive; Included.
apply Feq_reflexive; Included.
eapply Derivative_I_wdr.
apply Feq_plus with (F := F{*}PartInt G') (G := PartInt F'{*}G).
apply part_int_mult.
FEQ.
apply Feq_reflexive; Included.
apply part_int_mult.
apply Feq_reflexive; Included.
FEQ.
Deriv.
Qed.
Hypothesis Gbnd : bnd_away_zero I G.
Lemma Diffble_I_recip : Diffble_I Hab' {1/}G.
Proof.
elim diffG; intros G' derG.
cut (included I (Dom G)); [ intro Hg' | unfold I, Hab in |- *; Included ].
unfold I in Hg';
cut (∀ x : subset I, IMult (IntPartIR Hg') (IntPartIR Hg') x [#] [0]). intro H.
∃ (IInv (IDiv G' _ H)).
eapply Derivative_I_wdr.
apply part_int_inv with (F := PartInt (IDiv G' _ H)).
apply Feq_reflexive; Included.
eapply Derivative_I_wdr.
apply Feq_inv with (F := PartInt G'{/}PartInt (IMult (IntPartIR Hg') (IntPartIR Hg'))).
apply part_int_div.
apply Feq_reflexive; Included.
apply Feq_reflexive; simpl in |- *; Included.
red in |- *; intros.
split.
simpl in |- *; Included.
elim Gbnd; intros Hinc c.
elim c; clear c; intros c H0 H1.
∃ (c[*]c).
apply mult_resp_pos; assumption.
intros.
simpl in |- ×.
eapply leEq_wdr.
2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
apply mult_resp_leEq_both; auto; apply less_leEq; assumption.
eapply Derivative_I_wdr.
apply Feq_inv with (F := PartInt G'{/}G{*}G).
apply Feq_div.
Included.
apply Feq_reflexive; Included.
apply part_int_mult.
FEQ.
FEQ.
Deriv.
intro x.
simpl in |- ×.
apply mult_resp_ap_zero; apply bnd_imp_ap_zero with I; auto; apply scs_prf.
Qed.
End Operations.
Section Corollaries.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variables F G : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffG : Diffble_I Hab' G.
Lemma Diffble_I_minus : Diffble_I Hab' (F{-}G).
Proof.
apply Diffble_I_wd with (F{+}{--}G).
apply Diffble_I_plus.
assumption.
apply Diffble_I_inv; assumption.
FEQ.
Qed.
Lemma Diffble_I_scal : ∀ c : IR, Diffble_I Hab' (c{**}F).
Proof.
intro.
unfold Fscalmult in |- ×.
apply Diffble_I_mult.
apply Diffble_I_const.
assumption.
Qed.
Lemma Diffble_I_nth : ∀ n : nat, Diffble_I Hab' (F{^}n).
Proof.
intro.
induction n as [| n Hrecn].
eapply Diffble_I_wd.
2: apply FNth_zero'; Included.
apply Diffble_I_const.
eapply Diffble_I_wd.
2: apply FNth_mult'; Included.
apply Diffble_I_mult; assumption.
Qed.
Hypothesis Gbnd : bnd_away_zero I G.
Lemma Diffble_I_div : Diffble_I Hab' (F{/}G).
Proof.
apply Diffble_I_wd with (F{*}{1/}G).
apply Diffble_I_mult.
assumption.
apply Diffble_I_recip; assumption.
FEQ.
Qed.
End Corollaries.
Section Other_Properties.
Differentiability of families of functions is proved by
induction using the constant and addition rules.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Lemma Diffble_I_Sum0 : ∀ (f : nat → PartIR),
(∀ n, Diffble_I Hab' (f n)) → ∀ n, Diffble_I Hab' (FSum0 n f).
Proof.
intros f diffF.
induction n as [| n Hrecn].
apply Diffble_I_wd with (Fconst (S:=IR) [0]).
apply Diffble_I_const.
FEQ.
red in |- *; simpl in |- *; intros.
apply (diffble_imp_inc _ _ _ _ (diffF n)); assumption.
apply Diffble_I_wd with (FSum0 n f{+}f n).
apply Diffble_I_plus.
auto.
auto.
FEQ.
simpl in |- *; red in |- *; intros.
apply (diffble_imp_inc _ _ _ _ (diffF n0)); assumption.
simpl in |- ×.
apply bin_op_wd_unfolded; try apply Sum0_wd; intros; rational.
Qed.
Lemma Diffble_I_Sumx : ∀ n (f : ∀ i, i < n → PartIR),
(∀ i Hi, Diffble_I Hab' (f i Hi)) → Diffble_I Hab' (FSumx n f).
Proof.
intro; induction n as [| n Hrecn]; intros.
simpl in |- *; apply Diffble_I_const.
simpl in |- ×.
apply Diffble_I_plus; auto.
Qed.
Lemma Diffble_I_Sum : ∀ (f : nat → PartIR),
(∀ n, Diffble_I Hab' (f n)) → ∀ m n, Diffble_I Hab' (FSum m n f).
Proof.
intros.
eapply Diffble_I_wd.
2: apply Feq_symmetric; apply FSum_FSum0'; Included.
apply Diffble_I_minus; apply Diffble_I_Sum0; auto.
Qed.
End Other_Properties.
Finally, a differentiable function is continuous.
Let F be a partial function with derivative F' on I.
Lemma diffble_imp_contin_I : ∀ a b (Hab' : a [<] b) (Hab : a [<=] b) F,
Diffble_I Hab' F → Continuous_I Hab F.
Proof.
intros a b Hab' Hab F H.
apply deriv_imp_contin_I with Hab' (PartInt (ProjT1 H)).
apply projT2.
Qed.
Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
diffble_imp_contin_I: continuous.
Hint Immediate included_imp_deriv: derivate.