proposition: Lemma Derivative_power : forall (J : interval) pJ F F' G G', positive_fun J F -> Derivative J pJ F F' -> Derivative J pJ G G' -> Derivative J pJ (F{!}G) (G{*} (F{!} (G{-} [-C-][1]) {*}F') {+}F{!}G{*} (G'{*} (Logarithm[o]F))).
proof: Proof. intros J pJ F F' G G' H H0 H1. unfold FPower in |- *. assert (H2 : Derivative (openl [0]) I Logarithm {1/}FId). apply Derivative_Log. assert (H3 : Derivative realline I Expon Expon). apply Derivative_Exp. elim H; intros incF H'. elim H'; intros c H4 H5; clear incF H'. Derivative_Help. apply eq_imp_Feq. apply included_FMult. apply included_FComp. intros x H6. repeat split. apply (Derivative_imp_inc _ _ _ _ H1); auto. simpl in |- *. exists (Derivative_imp_inc _ _ _ _ H0 _ H6). apply Log_domain; apply less_leEq_trans with c; auto. intros; apply Exp_domain. intros x H6; simpl in |- *; repeat split. apply (Derivative_imp_inc _ _ _ _ H1); auto. exists (Derivative_imp_inc _ _ _ _ H0 _ H6). repeat split. intros; simpl in |- *. apply Greater_imp_ap; apply less_leEq_trans with c; auto. apply (Derivative_imp_inc' _ _ _ _ H0); auto. apply (Derivative_imp_inc' _ _ _ _ H1); auto. exists (Derivative_imp_inc _ _ _ _ H0 _ H6). intros; apply Log_domain; apply less_leEq_trans with c; auto. apply included_FPlus. apply included_FMult. Included. apply included_FMult. apply included_FComp. apply included_FMult. Included. apply included_FComp. Included. intros; apply Log_domain; apply less_leEq_trans with c; auto. intros; apply Exp_domain. Included. apply included_FMult. apply included_FComp. apply included_FMult. Included. apply included_FComp. Included. intros; apply Log_domain; apply less_leEq_trans with c; auto. intros; apply Exp_domain. apply included_FMult. Included. apply included_FComp. Included. intros; apply Log_domain; apply less_leEq_trans with c; auto. intros. astepl (Part _ _ (ProjIR1 Hx) [*]Part _ _ (ProjIR2 Hx)). elim Hx; intros Hx1 Hx2; clear Hx. astepl (Part _ _ Hx1[*]Part _ _ Hx2). astepl (Part _ _ (ProjT2 Hx1) [*]Part _ _ Hx2). elim Hx1; clear Hx1; intros Hx1 Hx3. astepl (Part _ (Part _ _ Hx1) Hx3[*]Part _ _ Hx2). generalize Hx3; clear Hx3. elim Hx1; intros Hx4 Hx5. intro; astepl (Part _ (Part _ _ (ProjIR1 (Hx4, Hx5)) [*] Part _ _ (ProjIR2 (Hx4, Hx5))) Hx3[*] Part _ _ Hx2). cut (Dom Expon (Part _ _ Hx4[*]Part _ _ Hx5)). intro H7. 2: apply dom_wd with (x := Part _ _ (ProjIR1 (Hx4, Hx5)) [*] Part _ _ (ProjIR2 (Hx4, Hx5))); algebra. astepl (Part _ (Part _ _ Hx4[*]Part _ _ Hx5) H7[*]Part _ _ Hx2). clear Hx3; rename H7 into Hx3. astepl (Part _ (Part _ _ Hx4[*]Part _ _ (ProjT2 Hx5)) Hx3[*]Part _ _ Hx2). generalize Hx3; clear Hx3. elim Hx5; intros Hx6 Hx7. intro; astepl (Part _ (Part _ _ Hx4[*]Part _ _ Hx7) Hx3[*]Part _ _ Hx2). set (A := Part _ (Part _ _ Hx4[*]Part _ _ Hx7) Hx3) in *. astepl (A[*] (Part _ _ (ProjIR1 Hx2) [+]Part _ _ (ProjIR2 Hx2))). elim Hx2; intros Hx8 Hx9. astepl (A[*] (Part _ _ Hx8[+]Part _ _ Hx9)). astepl (A[*] (Part _ _ (ProjIR1 Hx8) [*]Part _ _ (ProjIR2 Hx8) [+]Part _ _ Hx9)). elim Hx8; intros Hx10 Hx11. astepl (A[*] (Part _ _ Hx10[*]Part _ _ Hx11[+]Part _ _ Hx9)). astepl (A[*] (Part _ _ Hx10[*]Part _ _ Hx11[+] Part _ _ (ProjIR1 Hx9) [*]Part _ _ (ProjIR2 Hx9))). elim Hx9; intros Hx12 Hx13. astepl (A[*] (Part _ _ Hx10[*]Part _ _ Hx11[+]Part _ _ Hx12[*]Part _ _ Hx13)). astepl (A[*] (Part _ _ Hx10[*] (Part _ _ (ProjIR1 Hx11) [*]Part _ _ (ProjIR2 Hx11)) [+] Part _ _ Hx12[*]Part _ _ Hx13)). elim Hx11; intros Hx14 Hx15. apply eq_transitive_unfolded with (A[*] (Part _ _ Hx10[*] (Part _ _ Hx14[*]Part _ _ Hx15) [+] Part _ _ Hx12[*]Part _ _ Hx13)). apply mult_wd; algebra. astepl (A[*] (Part _ _ Hx10[*] (Part _ _ Hx14[*]Part _ _ Hx15) [+] Part _ _ Hx12[*]Part _ _ (ProjT2 Hx13))). elim Hx13; intros Hx16 Hx17. astepl (A[*] (Part _ _ Hx10[*] (Part _ _ Hx14[*]Part _ _ Hx15) [+] Part _ _ Hx12[*]Part _ _ Hx17)). astepl (A[*] (Part _ _ Hx10[*] (Part _ _ (ProjT2 Hx14) [*]Part _ _ Hx15) [+] Part _ _ Hx12[*]Part _ _ Hx17)). elim Hx14; intros Hx18 Hx19. astepl (A[*] (Part _ _ Hx10[*] (Part _ _ Hx19[*]Part _ _ Hx15) [+] Part _ _ Hx12[*]Part _ _ Hx17)). elim Hx19; intros Hx20 Hx21. assert (H7 : Dom G x). auto. assert (H8 : Dom F x). auto. cut ([0] [<] Part _ _ H8). intro H9. assert (H10 : Part _ _ H8 [#] [0]). apply Greater_imp_ap; auto. assert (H11 : Dom F' x). auto. assert (H12 : Dom G' x). auto. apply eq_transitive_unfolded with (Exp (Part _ _ H7[*]Log _ H9) [*] (Part _ _ H7[*] (([1][/] _[//]H10) [*]Part _ _ H11) [+] Part _ _ H12[*]Log _ H9)). unfold A, Log in |- *; simpl in |- *. repeat first [apply mult_wd | apply pfwdef | apply bin_op_wd_unfolded]; try reflexivity. clear Hx21 Hx20 Hx19 Hx18 Hx17 Hx16 Hx15 Hx14 Hx13 Hx12 Hx11 Hx10 Hx9 Hx8 A Hx3 Hx7 Hx6 Hx5 Hx4 Hx1 Hx2. astepr (Part _ _ (ProjIR1 Hx') [+]Part _ _ (ProjIR2 Hx')). elim Hx'; clear Hx'; intros Hx1 Hx2. astepr (Part _ _ Hx1[+]Part _ _ Hx2). astepr (Part _ _ Hx1[+]Part _ _ (ProjIR1 Hx2) [*]Part _ _ (ProjIR2 Hx2)). elim Hx2; clear Hx2; intros Hx2 Hx3. astepr (Part _ _ Hx1[+]Part _ _ Hx2[*]Part _ _ Hx3). astepr (Part _ _ Hx1[+] Part _ _ Hx2[*] (Part _ _ (ProjIR1 Hx3) [*]Part _ _ (ProjIR2 Hx3))). elim Hx3; clear Hx3; intros Hx3 Hx4. astepr (Part _ _ Hx1[+]Part _ _ Hx2[*] (Part _ _ H12[*]Part _ _ Hx4)); clear Hx3. astepr (Part _ _ Hx1[+]Part _ _ Hx2[*] (Part _ _ H12[*]Part _ _ (ProjT2 Hx4))). elim Hx4; clear Hx4; intros Hx3 Hx4. astepr (Part _ _ Hx1[+]Part _ _ Hx2[*] (Part _ _ H12[*]Part _ _ Hx4)). apply eq_transitive_unfolded with (Part _ _ Hx1[+]Part _ _ Hx2[*] (Part _ _ H12[*]Log _ H9)). 2: unfold Log in |- *; apply bin_op_wd_unfolded; algebra. clear Hx3 Hx4. astepr (Part _ _ Hx1[+]Part _ _ (ProjT2 Hx2) [*] (Part _ _ H12[*]Log _ H9)). elim Hx2; clear Hx2; intros Hx2 Hx3. astepr (Part _ _ Hx1[+]Part _ _ Hx3[*] (Part _ _ H12[*]Log _ H9)). generalize Hx3; clear Hx3. elim Hx2; clear Hx2; intros Hx4 Hx5 Hx3. assert (H13 : Dom Expon (Part _ _ Hx4[*]Part _ _ Hx5)). apply Exp_domain. astepr (Part _ _ Hx1[+] Part _ (Part _ _ (ProjIR1 (Hx4, Hx5)) [*] Part _ _ (ProjIR2 (Hx4, Hx5))) Hx3[*] (Part _ _ H12[*]Log _ H9)). apply eq_transitive_unfolded with (Part _ _ Hx1[+]Part _ _ H13[*] (Part _ _ H12[*]Log _ H9)). 2: apply bin_op_wd_unfolded; algebra. generalize H13; clear H13 Hx3. elim Hx5; clear Hx5; intros Hx5 Hx6 Hx3. astepr (Part _ _ Hx1[+] Part _ (Part _ _ Hx4[*]Part _ _ Hx6) Hx3[*] (Part _ _ H12[*]Log _ H9)). apply eq_transitive_unfolded with (Part _ _ Hx1[+]Exp (Part _ _ H7[*]Log _ H9) [*] (Part _ _ H12[*]Log _ H9)). 2: apply bin_op_wd_unfolded; [ algebra | unfold Log in |- *; simpl in |- * ]. 2: apply bin_op_wd_unfolded; algebra. eapply eq_transitive_unfolded. apply ring_dist_unfolded. apply bin_op_wd_unfolded. 2: apply eq_reflexive_unfolded. clear Hx3 Hx6 Hx5 Hx4. astepr (Part _ _ (ProjIR1 Hx1) [*]Part _ _ (ProjIR2 Hx1)). elim Hx1; clear Hx1; intros Hx1 Hx2. astepr (Part _ _ Hx1[*]Part _ _ Hx2). astepr (Part _ _ H7[*] (Part _ _ (ProjIR1 Hx2) [*]Part _ _ (ProjIR2 Hx2))). elim Hx2; clear Hx2 Hx1; intros Hx1 Hx2. astepr (Part _ _ H7[*] (Part _ _ Hx1[*]Part _ _ H11)). astepr (Part _ _ H7[*] (Part _ _ (ProjT2 Hx1) [*]Part _ _ H11)). elim Hx1; clear Hx1 Hx2; intros Hx1 Hx2. astepr (Part _ _ H7[*] (Part _ _ Hx2[*]Part _ _ H11)). apply eq_transitive_unfolded with (Part _ _ H7[*] (Exp (Part _ _ Hx1) [*]Part _ _ H11)). 2: simpl in |- *; algebra. clear Hx2. apply eq_transitive_unfolded with (Part _ _ H7[*] (Exp (Part _ _ (ProjIR1 Hx1) [*]Part _ _ (ProjIR2 Hx1)) [*]Part _ _ H11)). 2: apply mult_wdr; algebra. elim Hx1; clear Hx1; intros Hx1 Hx2. apply eq_transitive_unfolded with (Part _ _ H7[*] (Exp (Part _ _ Hx1[*]Part _ _ Hx2) [*]Part _ _ H11)). 2: apply mult_wdr; algebra. apply eq_transitive_unfolded with (Part _ _ H7[*] (Exp ((Part _ _ H7[-][1]) [*]Log _ H9) [*]Part _ _ H11)). 2: unfold Log in |- *; simpl in |- *. 2: apply mult_wdr; apply mult_wd; algebra. clear Hx1 Hx2. rstepl ((Exp (Part _ _ H7[*]Log _ H9) [/] _[//]H10) [*] (Part _ _ H7[*]Part _ _ H11)). rstepr (Exp ((Part _ _ H7[-][1]) [*]Log _ H9) [*] (Part _ _ H7[*]Part _ _ H11)). apply mult_wdl. apply eq_transitive_unfolded with (Exp (Part _ _ H7[*]Log _ H9[-]Log _ H9)). 2: apply Exp_wd; rational. astepr (Exp (G x H7[*]Log _ H9) [/] _[//]Exp_ap_zero (Log _ H9)). algebra. Transparent Logarithm. astepr (Part _ _ Hx16); auto. Opaque Logarithm. apply Derivative_comp with realline I; Deriv. apply Continuous_imp_maps_compacts_into. apply Continuous_mult. apply Derivative_imp_Continuous with pJ G'; auto. apply Continuous_comp with (openl [0]). apply maps_compacts_into_strict_imp_weak; apply positive_imp_maps_compacts_into; auto. apply Derivative_imp_Continuous with pJ F'; auto. apply Derivative_imp_Continuous with pJ F'; auto. apply Continuous_Log. apply Derivative_mult. auto. apply Derivative_comp with (openl [0]) I; Deriv. apply positive_imp_maps_compacts_into; auto. apply Derivative_imp_Continuous with pJ F'; auto. Qed.
imports: CoRN.transc.Exponential