Calculus Theorems
This file is intended to present a collection of miscellaneous, mostly technical results in differential calculus that are interesting or useful in future work.
We begin with some properties of continuous functions. Every continuous function commutes with the limit of a numerical sequence (sometimes called Heine continuity).
Lemma Continuous_imp_comm_Lim : forall F x e, 0 [<] e ->
Continuous ([⋅,⋅] (Lim x[-]e) (Lim x[+]e)) F -> forall Hx Hxn H,
F (Lim x) Hx [=] Lim (Build_CauchySeq IR (fun n => F (x n) (Hxn n)) H).
This is a tricky result: if F is continuous and positive in both [a,b]
and (b,c], then it is positive in [a,c].
Lemma Continuous_imp_pos : forall a b c (Hac : a [<=] c), a [<=] b -> b [<] c ->
forall F, Continuous_I Hac F -> (forall t, a [<=] t -> t [<=] b -> forall Ht, 0 [<] F t Ht) ->
(forall t, b [<] t -> t [<=] c -> forall Ht, 0 [<] F t Ht) -> forall t, a [<=] t -> t [<=] c -> forall Ht, 0 [<] F t Ht.
Similar results for increasing functions:
Lemma strict_inc_glues : forall a b c F (Hab : a [<=] b) (Hbc : b [<=] c) (Hac : a [<=] c),
⊆ (Compact Hac) (Dom F) ->
(forall x y, Compact Hab x -> Compact Hab y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
(forall x y, Compact Hbc x -> Compact Hbc y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall x y, Compact Hac x -> Compact Hac y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy.
Lemma strict_inc_glues' : forall a b c F, a [<] b -> b [<] c -> ⊆ ((⋅,⋅) a c) (Dom F) ->
(forall x y, (⋅,⋅] a b x -> (⋅,⋅] a b y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
(forall x y, [⋅,⋅) b c x -> [⋅,⋅) b c y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall x y, (⋅,⋅) a c x -> (⋅,⋅) a c y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy.
Lemma strict_dec_glues : forall a b c F (Hab : a [<=] b) (Hbc : b [<=] c) (Hac : a [<=] c),
⊆ (Compact Hac) (Dom F) ->
(forall x y, Compact Hab x -> Compact Hab y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) ->
(forall x y, Compact Hbc x -> Compact Hbc y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall x y, Compact Hac x -> Compact Hac y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy.
Lemma strict_dec_glues' : forall a b c F, a [<] b -> b [<] c -> ⊆ ((⋅,⋅) a c) (Dom F) ->
(forall x y, (⋅,⋅] a b x -> (⋅,⋅] a b y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) ->
(forall x y, [⋅,⋅) b c x -> [⋅,⋅) b c y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall x y, (⋅,⋅) a c x -> (⋅,⋅) a c y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy.
More on glueing intervals.
Lemma olor_pos_clor_nonneg : forall a b (F : PartIR),
(forall x, (⋅,⋅) a b x -> forall Hx, 0 [<] F x Hx) -> forall Ha,
0 [<=] F a Ha -> forall x, [⋅,⋅) a b x -> forall Hx, 0 [<=] F x Hx.
Lemma olor_pos_olcr_nonneg : forall a b (F : PartIR),
(forall x, (⋅,⋅) a b x -> forall Hx, 0 [<] F x Hx) -> forall Hb,
0 [<=] F b Hb -> forall x, (⋅,⋅] a b x -> forall Hx, 0 [<=] F x Hx.
Lemma olor_pos_clcr_nonneg : forall a b (F : PartIR), a [<] b ->
(forall x, (⋅,⋅) a b x -> forall Hx, 0 [<] F x Hx) -> forall Ha, 0 [<=] F a Ha -> forall Hb, 0 [<=] F b Hb ->
forall x, [⋅,⋅] a b x -> forall Hx, 0 [<=] F x Hx.
Any function that has the null function as its derivative must be constant.
As a corollary, two functions with the same derivative must differ
by a constant.
Lemma Feq_crit_with_const : forall J pJ F G H,
Derivative J pJ F H -> Derivative J pJ G H -> {c : IR | ≈ J (F{-}G) [-C-]c}.
This yields the following known result: any differential equation
of the form f'=g with initial condition f(a) = b has a unique solution.
Lemma Feq_criterium : forall J pJ F G H, Derivative J pJ F H -> Derivative J pJ G H ->
forall x, J x -> (forall Hx Hx', F x Hx [=] G x Hx') -> ≈ J F G.
Finally, a well known result: any function with a (strictly) positive
derivative is (strictly) increasing. Although the two lemmas look
quite similar the proofs are completely different, both from the
formalization and from the mathematical point of view.
Lemma Derivative_imp_resp_less : forall J pJ a b F F', Derivative J pJ F F' ->
a [<] b -> J a -> J b -> (forall contF', 0 [<] glb_funct _ _ (Min_leEq_Max a b) F' contF') ->
forall Ha Hb, F a Ha [<] F b Hb.
Lemma Derivative_imp_resp_leEq : forall J pJ a b F F', Derivative J pJ F F' ->
a [<=] b -> J a -> J b -> (forall contF', 0 [<=] glb_funct _ _ (Min_leEq_Max b a) F' contF') ->
forall Ha Hb, F a Ha [<=] F b Hb.
Lemma Derivative_imp_resp_less' : forall J pJ a b F F', Derivative J pJ F F' ->
a [<] b -> J a -> J b -> (forall contF', 0 [<=] glb_funct _ _ (Min_leEq_Max b a) F' contF') ->
forall Ha Hb, F a Ha [#] F b Hb -> F a Ha [<] F b Hb.
From these results we can finally prove that exponentiation to a
real power preserves the less or equal than relation!
Lemma nexp_resp_leEq_odd : forall n, odd n -> forall x y : IR, x [<=] y -> x[^]n [<=] y[^]n.
End Various_Theorems.