proposition: Lemma D_Rsqr_u_epsilon_2 : forall (eps : posreal) (t : R), (derive_pt (fun y : R => Rsqr (u eps y)) t (fct_der2 eps t) <= 2 * u0 t * vi)%R.
proof: Proof. intros; set (f := u eps). replace (derive_pt (fun y : R => Rsqr (f y)) t (fct_der2 eps t)) with (derive_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t (fct_der3 eps t)). replace (derive_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t (fct_der3 eps t)) with (2 * derive_pt xP t (xP_derivable t) * xP t + 2 * derive_pt yP t (yP_derivable t) * yP t)%R. rewrite (xP_derive t). rewrite (yP_derive t). assert (H0 := cond_x intr t). assert (H1 := cond_y intr t). cut (derive_pt (x intr) t (cond_diff (x intr) t) = derive_pt xi t (xi_derivable t)); [ intro | apply pr_nu ]. cut (derive_pt (y intr) t (cond_diff (y intr) t) = derive_pt yi t (yi_derivable t)); [ intro | apply pr_nu ]. rewrite <- H; rewrite <- H2; rewrite H1; rewrite H0. unfold vi in |- *. repeat rewrite Rmult_assoc. rewrite <- Rmult_plus_distr_l. apply Rmult_le_compat_l. left; prove_sup0. rewrite <- Rmult_plus_distr_l. rewrite (Rmult_comm (u0 t)); apply Rmult_le_compat_l. left; apply (TypeSpeed_pos (h intr)). generalize (sqrt_cauchy (cos (theta intr t)) (sin (theta intr t)) (xP t) (yP t)); rewrite (Rplus_comm (Rsqr (cos (theta intr t)))); rewrite sin2_cos2; rewrite sqrt_1; rewrite Rmult_1_l; intro H8; unfold u0 in |- *; assumption. set (H0 := xP_derivable t). set (H1 := yP_derivable t). symmetry in |- *; reg. unfold derive_pt in |- *; unfold derivable_pt_abs in |- *; cut (forall l : R, derivable_pt_lim (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t l <-> derivable_pt_lim (fun y : R => Rsqr (f y)) t l). intro; unfold projT1 in |- *. case (fct_der3 eps t); intros. case (fct_der2 eps t); intros. assert (H0 := H x). unfold derivable_pt_abs in d. elim H0; intros; fold f in d0. assert (H3 := H1 d). eapply uniqueness_limite. apply H3. apply d0. intro; unfold derivable_pt_lim in |- *. split; intros. elim (H eps0 H0); intros. exists x; intros; unfold f in |- *; unfold u in |- *. repeat rewrite Rsqr_sqrt. repeat rewrite Rplus_assoc. apply H1; assumption. repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr. repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr. elim (H eps0 H0); intros. exists x; intros; unfold f in H1; unfold u in H1. replace ((Rsqr (xP (t + h)) + (Rsqr (yP (t + h)) + Rsqr eps) - (Rsqr (xP t) + (Rsqr (yP t) + Rsqr eps))) / h - l)%R with ((Rsqr (sqrt (Rsqr (xP (t + h)) + Rsqr (yP (t + h)) + Rsqr eps)) - Rsqr (sqrt (Rsqr (xP t) + Rsqr (yP t) + Rsqr eps))) / h - l)%R. apply H1; assumption. repeat rewrite Rsqr_sqrt. repeat rewrite Rplus_assoc; reflexivity. repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr. repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr. Qed.
imports: Reals trajectory_const rrho trajectory_def constants