proposition: Lemma Sin_plus_Taylor_bnd_lft : forall y : IR, Taylor_bnd (F' y).
proof: Proof. clear F G G'; intros. apply bnd_imp_Taylor_bnd with (FAbs (Sine[o]FId{+} [-C-]y) {+}FAbs (Cosine[o]FId{+} [-C-]y)). intro; apply four_ind with (P := fun n : nat => forall (x : IR) Hx Hx', AbsIR (F' y n x Hx) [<=] AbsIR ((FAbs (Sine[o]FId{+} [-C-]y) {+}FAbs (Cosine[o]FId{+} [-C-]y)) x Hx')). intros. unfold F' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl (AbsIR (Sine (x[+]y) (ProjT2 Hx)) [+][0]). apply plus_resp_leEq_both. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR1 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply FAbs_nonneg. intros. unfold F' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl ([0][+]AbsIR (Cosine (x[+]y) (ProjT2 Hx))). apply plus_resp_leEq_both. apply FAbs_nonneg. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR2 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. intros. unfold F' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl (AbsIR [--] (Sine (x[+]y) (ProjT2 Hx)) [+][0]). apply leEq_wdl with (AbsIR (Sine (x[+]y) (ProjT2 Hx)) [+][0]). apply plus_resp_leEq_both. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR1 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply FAbs_nonneg. apply bin_op_wd_unfolded. apply AbsIR_inv. algebra. intros. unfold F' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl ([0][+]AbsIR [--] (Cosine (x[+]y) (ProjT2 Hx))). apply leEq_wdl with ([0][+]AbsIR (Cosine (x[+]y) (ProjT2 Hx))). apply plus_resp_leEq_both. apply FAbs_nonneg. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR2 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply bin_op_wd_unfolded. algebra. apply AbsIR_inv. auto. cut (maps_compacts_into_weak realline realline (Fid IR{+} [-C-]y)); intros. apply Continuous_plus; apply Continuous_abs; apply Continuous_comp with realline; Contin. intros a b Hab H. exists (a[+]y); exists (b[+]y). cut (a[+]y [<=] b[+]y). intro H0. exists H0. split. Included. intros x Hx H1; inversion_clear H1. split. simpl in |- *; apply plus_resp_leEq; auto. simpl in |- *; apply plus_resp_leEq; auto. apply plus_resp_leEq; auto. apply four_induction with (P := fun n : nat => included (fun _ : IR => True) (Dom (F' y n))); auto; unfold F' in |- *; Included. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)