proposition: Lemma bellcurve_series_convergent_IR : fun_series_convergent_IR (olor ([--][1]) [1]) (fun (i:nat) => ([--][1])[^]i{**}Fid IR{^}(2*i)).
proof: Proof. apply fun_series_convergent_wd_IR with (fun i => Fid IR{^}i[o]({--}(Fid IR{^}2))). intros n. FEQ. change ([--]([1][*]x[*]x)[^]n[=]([--][1])[^]n[*]x[^](2*n)). rstepl (([--][1][*](x[*]x))[^]n). stepl (([--][1])[^]n[*]((x[*]x)[^]n)); [| now apply eq_symmetric; apply mult_nexp]. apply mult_wdr. replace (2*n)%nat with (n+n)%nat by auto with *. eapply eq_transitive. apply mult_nexp. apply nexp_plus. apply FSeries_Sum_comp_conv with (olor [--][1] [1]); [|Contin|apply fun_power_series_conv_IR]. intros a b Hab Hinc. set (c:=Max (AbsIR a) (AbsIR b)). exists ([--](c[^]2)). exists (c[^]2). assert (X:[--](c[^]2)[<=]c[^]2). apply leEq_transitive with ([0]:IR). rstepr ([--][0]:IR). apply inv_resp_leEq. apply sqr_nonneg. apply sqr_nonneg. exists X. assert (A0:(c[^]2)[<][1]). rstepr ([1][^]2:IR). unfold c. apply nexp_resp_less. auto with *. eapply leEq_transitive. apply AbsIR_nonneg. apply lft_leEq_Max. apply Max_less; [destruct (Hinc _ (compact_inc_lft _ _ Hab)) |destruct (Hinc _ (compact_inc_rht _ _ Hab))]; apply AbsIR_less; assumption. assert (A1:[--][1][<][--](c[^]2)). apply inv_resp_less. assumption. split. intros d [Hd0 Hd1]. split. apply less_leEq_trans with ([--](c[^]2)); assumption. apply leEq_less_trans with (c[^]2); assumption. intros x Hx [Hx0 Hx1]. simpl. cut (AbsSmall (c[^]2) ([--](x[^]2))). intros [A B]; split; assumption. apply inv_resp_AbsSmall. rstepl (c[*]c). rstepr (x[*]x). cut (AbsSmall c x). intros; apply mult_AbsSmall; assumption. unfold c. split. rstepr ([--][--]x). apply inv_resp_leEq. eapply leEq_transitive;[|apply lft_leEq_Max]. eapply leEq_transitive;[|apply inv_leEq_AbsIR]. apply inv_resp_leEq. assumption. eapply leEq_transitive;[|apply rht_leEq_Max]. eapply leEq_transitive;[|apply leEq_AbsIR]. assumption. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac