proposition: Lemma differentiable_pt_lim_mult : forall f1 f2 x v l1 l2, differentiable_pt_lim f1 x v l1 -> differentiable_pt_lim f2 x v l2 -> differentiable_pt_lim (f1 * f2) x v (l1 * f2 x + f1 x * l2).
proof: Proof. intros f1 f2 x v l1 l2 Hf1 Hf2 v_neq eps eps_pos. assert (Hrew : forall h, h <> 0 -> ((f1 * f2)%F (x + h * v) - (f1 * f2)%F x) / (h * v) - (l1 * f2 x + f1 x * l2) = ((f1 (x + h * v) - f1 x) / (h * v)) * f2 (x + h * v) - l1 * f2 (x + h * v) + l1 * f2 (x + h * v) - l1 * f2 x + (f1 x) * (f2 (x + h * v) - f2 x) / (h * v) - (f1 x) * l2). clear - v_neq. intros h h_neq. unfold Cminus, Cdiv, mult_fct ; ring. assert (Main : forall h : C, h <> 0 ->((f1 * f2)%F (x + h * v) - (f1 * f2)%F x) / (h * v) - (l1 * f2 x + f1 x * l2) = ((f1 (x + h * v) - f1 x) / (h * v) - l1) * f2 x + ((f1 (x + h * v) - f1 x) / (h * v) - l1) * (f2 (x + h*v) - f2 x) + l1 * (f2 (x + h * v) - f2 x) + f1 x * ((f2 (x + h * v) - f2 x) / (h * v) - l2)). clear - v_neq Hrew. intros h h_neq. unfold Cminus, Cdiv, mult_fct ; ring. clear Hrew. destruct (Ceq_dec l1 0) as [l1_eq | l1_neq]. destruct (Ceq_dec (f1 x) 0) as [f1_eq | f1_neq]. destruct (Ceq_dec (f2 x) 0) as [f2_eq | f2_neq]. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (Rle_dec 1 eps) as [eps_lb | eps_ub]. destruct (Hf1 v_neq (Rmin 1 eps)) as [delta1 Hdelta1] ; [apply Rmin_pos ; lra |]. destruct (differentiable_continuous_along_axis f2 x v Hf2' (Rmin 1 eps)%R) as [delta2 Hdelta2] ; [apply Rmin_pos ; lra |]. pose (delta := Rmin delta1 delta2) ; assert (delta_pos : 0 < delta) by (apply Rmin_pos ; [apply delta1 | apply delta2]). exists (mkposreal delta delta_pos) ; intros h h_neq h_ub. rewrite Main ; clear Main ; repeat rewrite l1_eq, f1_eq, f2_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r. apply Rlt_le_trans with 1%R ; [| assumption]. rewrite Cnorm_Cmult ; apply Rle_lt_trans with (Cnorm (f2 (x + h * v) - 0)). rewrite <- Rmult_1_l ; apply Rmult_le_compat_r ; [apply Cnorm_pos |]. apply Rle_trans with (Rmin 1 eps) ; [left ; apply Hdelta1 | apply Rmin_l]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. apply Rlt_le_trans with (Rmin 1 eps) ; [simpl in Hdelta2 ; unfold C_dist in Hdelta2 ; apply Hdelta2 | apply Rmin_l]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. apply IRC_neq_0_compat ; assumption. assert (eps_lt_1 := Rnot_le_lt _ _ eps_ub) ; clear eps_ub. assert (eps_2_lt_eps : eps * eps < eps). rewrite <- Rmult_1_r ; apply Rmult_lt_compat_l ; assumption. destruct (Hf1 v_neq eps eps_pos) as [delta1 Hdelta1]. destruct (differentiable_continuous_along_axis f2 x v Hf2' eps eps_pos) as [delta2 Hdelta2]. pose (delta := Rmin delta1 delta2) ; assert (delta_pos : 0 < delta) by (apply Rmin_pos ; [apply delta1 | apply delta2]). exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite l1_eq, f1_eq, f2_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r. rewrite Cnorm_Cmult ; apply Rlt_trans with (eps * eps)%R ; [| assumption] ; clear eps_lt_1 eps_2_lt_eps. apply Rle_lt_trans with (eps * Cnorm (f2 (x + h * v)%C - C0))%R. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. left ; apply Hdelta1. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. apply Rmult_lt_compat_l ; [assumption |]. simpl in Hdelta2 ; unfold C_dist in Hdelta2 ; apply Hdelta2. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. destruct (Hf1 v_neq (Rmin (eps/2)%R ((eps/2) / Cnorm (f2 x)))) as [delta1 Hdelta1]. apply Rmin_pos ; [lra |]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' R1 Rlt_0_1) as [delta2 Hdelta2]. pose (delta := Rmin delta1 delta2) ; assert (delta_pos : 0 < delta) by (apply Rmin_pos ; [apply delta1 | apply delta2]). exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite l1_eq, f1_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rle_lt_trans with (Cnorm (f1 (x + h * v)%C / (h * v) * f2 x) + Cnorm (f1 (x + h * v)%C / (h * v) * (f2 (x + h * v)%C - f2 x)))%R. apply Cnorm_triang. apply Rlt_trans with (Cnorm (f1 (x + h * v)%C / (h * v) * f2 x) + eps / 2)%R. apply Rplus_lt_compat_l. rewrite Cnorm_Cmult. apply Rle_lt_trans with (Cnorm (f1 (x + h * v)%C / (h * v)))%R. rewrite <- Rmult_1_r ; apply Rmult_le_compat_l ; [apply Cnorm_pos |]. left ; simpl in Hdelta2 ; unfold C_dist in Hdelta2 ; apply Hdelta2. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. apply Rlt_le_trans with (Rmin (eps / 2) (eps / 2 / Cnorm (f2 x))) ; [| apply Rmin_l]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v) - 0) / (h * v) - 0)). right ; repeat rewrite Cminus_0_r ; reflexivity. apply Hdelta1. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [| right ; field]. apply Rplus_lt_compat_r. apply Rlt_le_trans with ((eps / 2 / Cnorm (f2 x)) * Cnorm (f2 x))%R. rewrite Cnorm_Cmult ; apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt ; assumption |]. apply Rlt_le_trans with (Rmin (eps / 2) (eps / 2 / Cnorm (f2 x))) ; [| apply Rmin_r]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C - 0) / (h * v) - 0))%R ; [right ; repeat rewrite Cminus_0_r ; reflexivity |] ; apply Hdelta1. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. right ; unfold Rdiv ; repeat rewrite Rmult_assoc ; rewrite Rinv_l. ring. apply Cnorm_no_R0 ; assumption. destruct (Ceq_dec (f2 x) 0) as [f2_eq | f2_neq]. destruct (Hf1 v_neq (eps/2)%R) as [delta1 Hdelta1] ; [lra |]. destruct (Hf2 v_neq ((eps / 2) / Cnorm (f1 x))%R) as [delta2 Hdelta2]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' R1 Rlt_0_1) as [delta3 Hdelta3]. pose (delta := Rmin delta1 (Rmin delta2 delta3)) ; assert (delta_pos : 0 < delta) by (repeat apply Rmin_pos ; [apply delta1 | apply delta2 | apply delta3]). exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite l1_eq, f2_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * f2 (x + h * v)%C) + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R ; [apply Cnorm_triang |]. apply Rlt_trans with (eps / 2 + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R. apply Rplus_lt_compat_r. rewrite Cnorm_Cmult ; apply Rle_lt_trans with (eps / 2 * Cnorm (f2 (x + h * v)%C))%R. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. apply Rle_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) - C0))%R ; [right ; rewrite Cminus_0_r ; reflexivity | left ; apply Hdelta1]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_lt_compat_l ; [lra |]. apply Rle_lt_trans with (dist C_met (f2 (x + h * v)) C0) ; [right ; simpl ; unfold C_dist ; rewrite Cminus_0_r ; reflexivity | apply Hdelta3]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; [apply Rmin_r | apply Rmin_r]]. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [| right ; field]. apply Rplus_lt_compat_l ; rewrite Cnorm_Cmult. apply Rlt_le_trans with (Cnorm (f1 x) * (/Cnorm (f1 x) * eps / 2))%R. apply Rmult_lt_compat_l ; [apply Cnorm_pos_lt ; assumption |]. apply Rlt_le_trans with (eps / 2 / Cnorm (f1 x))%R ; [| right ; field]. apply Rle_lt_trans with (Cnorm ((f2 (x + h * v) - 0) / (h * v) - l2)) ; [right ; rewrite Cminus_0_r ; reflexivity |] ; apply Hdelta2. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; [apply Rmin_r | apply Rmin_l]]. apply Cnorm_no_R0 ; assumption. right ; field ; apply Cnorm_no_R0 ; assumption. destruct (Hf1 v_neq (Rmin(eps/3) ((eps/3) / Cnorm (f2 x)))%R) as [delta1 Hdelta1]. apply Rmin_pos ; [lra |] ; apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. destruct (Hf2 v_neq ((eps / 3) / Cnorm (f1 x))%R) as [delta2 Hdelta2]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' R1 Rlt_0_1) as [delta3 Hdelta3]. pose (delta := Rmin delta1 (Rmin delta2 delta3)) ; assert (delta_pos : 0 < delta) by (repeat apply Rmin_pos ; [apply delta1 | apply delta2 | apply delta3]). exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite l1_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rlt_le_trans with (eps/3 + eps/3 + eps/3)%R ; [| right ; field]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * f2 x + (f1 (x + h * v)%C - f1 x) / (h * v) * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [apply Cnorm_triang |]. apply Rlt_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * f2 x + (f1 (x + h * v)%C - f1 x) / (h * v) * (f2 (x + h * v)%C - f2 x)) + eps / 3)%R. apply Rplus_lt_compat_l. rewrite Cnorm_Cmult ; apply Rlt_le_trans with (Cnorm (f1 x) * (eps / 3 / Cnorm (f1 x)))%R. apply Rmult_lt_compat_l ; [apply Cnorm_pos_lt ; assumption |]. apply Hdelta2. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; [apply Rmin_r | apply Rmin_l]]. right ; field ; apply Cnorm_no_R0 ; assumption. apply Rplus_lt_compat_r. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * f2 x) + Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * (f2 (x + h * v)%C - f2 x)))%R ; [apply Cnorm_triang |]. apply Rlt_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) * f2 x) + eps / 3)%R. apply Rplus_lt_compat_l. rewrite Cnorm_Cmult ; apply Rle_lt_trans with (eps / 3 * Cnorm (f2 (x + h * v)%C - f2 x))%R. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. apply Rle_trans with (Rmin (eps / 3) (eps / 3 / Cnorm (f2 x))) ; [| apply Rmin_l]. apply Rle_trans with (Cnorm ((f1 (x + h * v)%C - f1 x) / (h * v) - 0))%R ; [right ; rewrite Cminus_0_r ; reflexivity |] ; left ; apply Hdelta1. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_lt_compat_l ; [lra |] ; simpl in Hdelta3 ; unfold C_dist in Hdelta3 ; apply Hdelta3. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; apply Rmin_r]. apply Rplus_lt_compat_r ; rewrite Cnorm_Cmult. apply Rlt_le_trans with ((eps / 3 / Cnorm (f2 x)) * Cnorm (f2 x))%R. apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt ; assumption |]. apply Rlt_le_trans with (Rmin (eps / 3) (eps / 3 / Cnorm (f2 x))) ; [| apply Rmin_r]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v) - f1 x) / (h * v) - 0)) ; [right ; rewrite Cminus_0_r ; reflexivity |]. apply Hdelta1. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. right ; field ; apply Cnorm_no_R0 ; assumption. destruct (Ceq_dec (f1 x) 0) as [f1_eq | f1_neq]. destruct (Ceq_dec (f2 x) 0) as [f2_eq | f2_neq]. destruct (Hf1 v_neq (eps / 2)%R) as [delta1 Hdelta1] ; [lra |]. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' (Rmin R1 ((eps / 2) / Cnorm l1))) as [delta2 Hdelta2]. apply Rmin_pos ; [lra |]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; assumption]. pose (delta := Rmin delta1 delta2) ; assert (delta_pos : 0 < delta) by (apply Rmin_pos ; [apply delta1 | apply delta2]) ; exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite f1_eq, f2_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * f2 (x + h * v)%C) + Cnorm (l1 * f2 (x + h * v)%C))%R ; [apply Cnorm_triang |]. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [| right ; field]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * f2 (x + h * v)%C) + eps / 2)%R. apply Rplus_le_compat_l. rewrite Cnorm_Cmult ; apply Rle_trans with (Cnorm l1 * ((eps / 2) / Cnorm l1))%R. apply Rmult_le_compat_l ; [apply Cnorm_pos |]. apply Rle_trans with (Rmin 1 (eps / 2 / Cnorm l1)) ; [| apply Rmin_r]. apply Rle_trans with (dist C_met (f2 (x + h * v)) C0) ; [simpl ; unfold C_dist ; right ; rewrite Cminus_0_r ; reflexivity | left ; apply Hdelta2]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. right ; field ; apply Cnorm_no_R0 ; assumption. apply Rplus_lt_compat_r ; rewrite Cnorm_Cmult ; apply Rle_lt_trans with (eps / 2 * Cnorm (f2 (x + h * v)%C))%R. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. apply Rle_trans with (Cnorm ((f1 (x + h * v) - 0) / (h * v) - l1)) ; [rewrite Cminus_0_r ; right ; reflexivity | left ; apply Hdelta1]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_lt_compat_l ; [lra |]. apply Rle_lt_trans with (dist C_met (f2 (x + h * v)) C0) ; [simpl ; unfold C_dist ; rewrite Cminus_0_r ; right ; reflexivity |]. apply Rlt_le_trans with (Rmin 1 (eps / 2 / Cnorm l1)) ; [apply Hdelta2 | apply Rmin_l]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. destruct (Hf1 v_neq (Rmin (eps / 3) (eps / 3 / Cnorm (f2 x)))) as [delta1 Hdelta1]. apply Rmin_pos ; [lra |] ; apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' (Rmin 1 (eps / 3 / Cnorm l1))) as [delta2 Hdelta2]. apply Rmin_pos ; [apply Rlt_0_1 | apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption]. pose (delta := Rmin delta1 delta2) ; assert (delta_pos : 0 < delta) by (apply Rmin_pos ; [apply delta1 | apply delta2]) ; exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite f1_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * f2 x) + Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * (f2 (x + h * v)%C - f2 x) + l1 * (f2 (x + h * v)%C - f2 x)))%R ; [rewrite Cadd_assoc ; apply Cnorm_triang |]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * f2 x) + Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * (f2 (x + h * v)%C - f2 x)) + Cnorm (l1 * (f2 (x + h * v)%C - f2 x)))%R. rewrite Rplus_assoc ; apply Rplus_le_compat_l ; apply Cnorm_triang. apply Rlt_trans with (eps/3 + Cnorm ((f1 (x + h * v)%C / (h * v) - l1) * (f2 (x + h * v)%C - f2 x)) + Cnorm (l1 * (f2 (x + h * v)%C - f2 x)))%R. repeat apply Rplus_lt_compat_r ; rewrite Cnorm_Cmult ; apply Rlt_le_trans with ((eps / 3 / Cnorm (f2 x)) * Cnorm (f2 x))%R. apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt ; assumption |]. apply Rlt_le_trans with (Rmin (eps / 3) (eps / 3 / Cnorm (f2 x))) ; [| apply Rmin_r]. apply Rle_lt_trans with (Cnorm ((f1 (x + h * v) - 0) / (h * v) - l1)) ; [rewrite Cminus_0_r ; right ; reflexivity | apply Hdelta1]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. right ; field ; apply Cnorm_no_R0 ; assumption. apply Rlt_trans with (eps / 3 + eps / 3 + Cnorm (l1 * (f2 (x + h * v)%C - f2 x)))%R ; [apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l |]. rewrite Cnorm_Cmult ; apply Rle_lt_trans with (eps / 3 * Cnorm ((f2 (x + h * v)%C - f2 x)))%R ; [apply Rmult_le_compat_r ; [apply Cnorm_pos |]|]. apply Rle_trans with (Rmin (eps / 3) (eps / 3 / Cnorm (f2 x))) ; [| apply Rmin_l] ; apply Rle_trans with (Cnorm ((f1 (x + h * v)%C - C0) / (h * v) - l1))%R ; [right ; rewrite Cminus_0_r ; reflexivity | left ; apply Hdelta1]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_lt_compat_l ; [lra |]. apply Rle_lt_trans with (dist C_met (f2 (x + h * v)) (f2 x)) ; [right ; simpl ; unfold C_dist ; reflexivity |]. apply Rlt_le_trans with (Rmin 1 (eps / 3 / Cnorm l1)) ; [apply Hdelta2 | apply Rmin_l]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3)%R ; [apply Rplus_lt_compat_l | right ; field]. rewrite Cnorm_Cmult ; apply Rlt_le_trans with (Cnorm l1 * (eps / 3 / Cnorm l1))%R. apply Rmult_lt_compat_l ; [apply Cnorm_pos_lt ; assumption |]. apply Rle_lt_trans with (dist C_met (f2 (x + h * v)) (f2 x)) ; [simpl ; unfold C_dist ; right ; reflexivity | apply Rlt_le_trans with (Rmin 1 (eps / 3 / Cnorm l1)) ; [apply Hdelta2 | apply Rmin_r]]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_r]. right ; field ; apply Cnorm_no_R0 ; assumption. destruct (Ceq_dec (f2 x) 0) as [f2_eq | f2_neq]. destruct (Hf1 v_neq (eps / 3)%R) as [delta1 Hdelta1] ; [lra |]. destruct (Hf2 v_neq (eps / 3 / Cnorm (f1 x))%R) as [delta2 Hdelta2]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' (Rmin 1 (eps / 3 / Cnorm l1))) as [delta3 Hdelta3]. apply Rmin_pos ; [apply Rlt_0_1 |] ; apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. pose (delta := Rmin delta1 (Rmin delta2 delta3)) ; assert (delta_pos : 0 < delta) by (repeat apply Rmin_pos ; [apply delta1 | apply delta2 | apply delta3]) ; exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main ; repeat rewrite f2_eq in * ; repeat rewrite Cmult_0_r ; repeat rewrite Cmult_0_l ; repeat rewrite Cadd_0_l ; repeat rewrite Cadd_0_r ; repeat rewrite Cminus_0_r in *. apply Rle_lt_trans with (Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * f2 (x + h * v)%C + l1 * f2 (x + h * v)%C) + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R ; [apply Cnorm_triang |] ; apply Rle_lt_trans with (Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * f2 (x + h * v)%C) + Cnorm (l1 * f2 (x + h * v)%C) + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R ; [apply Rplus_le_compat_r ; apply Cnorm_triang |]. apply Rle_lt_trans with (eps / 3 + Cnorm (l1 * f2 (x + h * v)%C) + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R ; [repeat apply Rplus_le_compat_r |]. rewrite Cnorm_Cmult ; apply Rle_trans with (eps / 3 * Cnorm (f2 (x + h * v)%C))%R ; [apply Rmult_le_compat_r ; [apply Cnorm_pos | left ; apply Hdelta1] |]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_le_compat_l ; [lra |] ; apply Rle_trans with (dist C_met (f2 (x + h * v)) C0) ; [simpl ; unfold C_dist ; rewrite Cminus_0_r ; right ; reflexivity |] ; apply Rle_trans with (Rmin 1 (eps / 3 / Cnorm l1)) ; [left ; apply Hdelta3 | apply Rmin_l]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; apply Rmin_r]. apply Rle_lt_trans with (eps / 3 + eps / 3 + Cnorm (f1 x * (f2 (x + h * v)%C / (h * v) - l2)))%R ; [apply Rplus_le_compat_r ; apply Rplus_le_compat_l |]. rewrite Cnorm_Cmult ; apply Rle_trans with (Cnorm l1 * (eps / 3 / Cnorm l1))%R ; [apply Rmult_le_compat_l ; [apply Cnorm_pos|] |]. apply Rle_trans with (dist C_met (f2 (x + h * v)) C0) ; [simpl ; unfold C_dist ; rewrite Cminus_0_r ; right ; reflexivity |] ; apply Rle_trans with (Rmin 1 (eps / 3 / Cnorm l1)) ; [left ; apply Hdelta3 | apply Rmin_r]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; apply Rmin_r]. right ; field ; apply Cnorm_no_R0 ; assumption. apply Rlt_le_trans with (eps / 3 + eps / 3 + eps /3)%R ; [repeat rewrite Rplus_assoc ; repeat apply Rplus_lt_compat_l | right ; field]. rewrite Cnorm_Cmult ; apply Rlt_le_trans with (Cnorm (f1 x) * (eps / 3 / Cnorm (f1 x)))%R. apply Rmult_lt_compat_l ; [apply Cnorm_pos_lt ; assumption |]. apply Rle_lt_trans with (Cnorm ((f2 (x + h * v)%C - 0) / (h * v) - l2))%R ; [rewrite Cminus_0_r ; right ; reflexivity | apply Hdelta2]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; [apply Rmin_r | apply Rmin_l]]. right ; field ; apply Cnorm_no_R0 ; assumption. destruct (Hf1 v_neq (Rmin (eps / 4) (eps / 4 / Cnorm (f2 x)))) as [delta1 Hdelta1]. apply Rmin_pos ; [lra |] ; apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. destruct (Hf2 v_neq (eps / 4 / Cnorm (f1 x))%R) as [delta2 Hdelta2]. apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. assert (Hf2' : differentiable_pt f2 x v). exists l2 ; apply Hf2. destruct (differentiable_continuous_along_axis f2 x v Hf2' (Rmin 1 (eps / 4 / Cnorm l1))) as [delta3 Hdelta3]. apply Rmin_pos ; [apply Rlt_0_1 |] ; apply Rmult_lt_0_compat ; [lra | apply Rinv_0_lt_compat ; apply Cnorm_pos_lt] ; assumption. pose (delta := Rmin delta1 (Rmin delta2 delta3)) ; assert (delta_pos : 0 < delta) by (repeat apply Rmin_pos ; [apply delta1 | apply delta2 | apply delta3]) ; exists (mkposreal delta delta_pos) ; intros h h_neq h_ub ; rewrite Main ; [| apply IRC_neq_0_compat ; assumption] ; clear Main. apply Rle_lt_trans with (Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * f2 x + ((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * (f2 (x + h * v)%C - f2 x) + l1 * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [apply Cnorm_triang |]. apply Rle_lt_trans with (Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * f2 x + ((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * (f2 (x + h * v)%C - f2 x)) + Cnorm ( l1 * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [apply Rplus_le_compat_r ; apply Cnorm_triang |]. apply Rle_lt_trans with (Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * f2 x) + Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * (f2 (x + h * v)%C - f2 x)) + Cnorm ( l1 * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [repeat apply Rplus_le_compat_r ; apply Cnorm_triang |]. apply Rle_lt_trans with (eps / 4 + Cnorm (((f1 (x + h * v)%C - f1 x) / (h * v) - l1) * (f2 (x + h * v)%C - f2 x)) + Cnorm (l1 * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [repeat apply Rplus_le_compat_r |]. rewrite Cnorm_Cmult ; apply Rle_trans with ((eps / 4 / Cnorm (f2 x)) * Cnorm (f2 x))%R ; [apply Rmult_le_compat_r ; [apply Cnorm_pos |] |]. apply Rle_trans with (Rmin (eps / 4) (eps / 4 / Cnorm (f2 x))) ; [left ; apply Hdelta1 | apply Rmin_r]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. right ; field ; apply Cnorm_no_R0 ; assumption. apply Rle_lt_trans with (eps / 4 + eps / 4 + Cnorm (l1 * (f2 (x + h * v)%C - f2 x)) + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [repeat apply Rplus_le_compat_r ; apply Rplus_le_compat_l |]. rewrite Cnorm_Cmult ; apply Rle_trans with (eps / 4 * Cnorm ((f2 (x + h * v)%C - f2 x)))%R ; [apply Rmult_le_compat_r ; [apply Cnorm_pos |] |]. apply Rle_trans with (Rmin (eps / 4) (eps / 4 / Cnorm (f2 x))) ; [left ; apply Hdelta1 | apply Rmin_l]. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rmin_l]. rewrite <- Rmult_1_r ; apply Rmult_le_compat_l ; [lra |] ; apply Rle_trans with (Rmin 1 (eps / 4 / Cnorm l1)) ; [| apply Rmin_l]. apply Rle_trans with (dist C_met (f2 (x + h * v)) (f2 x)) ; [simpl ; unfold C_dist ; right ; reflexivity | left ; apply Hdelta3]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; apply Rmin_r]. apply Rle_lt_trans with (eps / 4 + eps / 4 + eps / 4 + Cnorm (f1 x * ((f2 (x + h * v)%C - f2 x) / (h * v) - l2)))%R ; [repeat apply Rplus_le_compat_r ; apply Rplus_le_compat_l |]. rewrite Cnorm_Cmult ; apply Rle_trans with (Cnorm l1 * (eps / 4 / Cnorm l1))%R ; [apply Rmult_le_compat_l ; [apply Cnorm_pos |] | right ; field ; apply Cnorm_no_R0 ; assumption]. apply Rle_trans with (Rmin 1 (eps / 4 / Cnorm l1)) ; [| apply Rmin_r]. apply Rle_trans with (dist C_met (f2 (x + h * v)) (f2 x)) ; [simpl ; unfold C_dist ; right ; reflexivity | left ; apply Hdelta3]. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; apply Rmin_r]. apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4)%R ; [| right ; field]. apply Rplus_lt_compat_l. rewrite Cnorm_Cmult ; apply Rlt_le_trans with (Cnorm (f1 x) * (eps / 4 / Cnorm (f1 x)))%R ; [apply Rmult_lt_compat_l ; [apply Cnorm_pos_lt ; assumption |] | right ; field ; apply Cnorm_no_R0 ; assumption] ; apply Hdelta2. assumption. apply Rlt_le_trans with delta ; [apply h_ub | apply Rle_trans with (Rmin delta2 delta3) ; [apply Rmin_r | apply Rmin_l]]. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def