proposition: Lemma bellcurve_series : forall (Hs:fun_series_convergent_IR (olor ([--][1]) [1]) (fun (i:nat) => ([--][1])[^]i{**}Fid IR{^}(2*i))), Feq (olor ([--][1]) [1]) (FSeries_Sum Hs) ({1/}([-C-][1]{+}FId{^}2)).
proof: Proof. intros Hs. split. simpl. apply included_refl. split. apply included_trans with realline. intros x _; constructor. apply Continuous_imp_inc. apply ArcTan_def_lemma. intros c [Hc0 Hc1] D0 D1. assert (X:AbsIR ([--](c[^]2))[<][1]). csetoid_rewrite_rev (AbsIR_inv (c[^]2)). csetoid_rewrite (AbsIR_nexp_op 2 c). rstepr ([1][^]2:IR). apply nexp_resp_less. auto with *. apply AbsIR_nonneg. apply AbsIR_less; assumption. simpl. generalize (ext2 (S:=IR) (P:=Conj (fun _ : IR => True) (fun _ : IR => True)) (R:=fun (x : IR) (_ : Conj (fun _ : IR => True) (fun _ : IR => True) x) => [1][+][1][*]x[*]x[#][0]) (x:=c) D1). intros H. assert (Y:[1][-]([--](c[^]2))[#][0]). rstepl ([1][+][1][*]c[*]c). assumption. rstepr ([1][/]([1][-]([--](c[^]2)))[//]Y). stepr (series_sum (power_series [--](c[^]2)) (power_series_conv [--](c[^]2) X)); [| now apply (power_series_sum ([--](c[^]2)) X Y (power_series_conv _ X))]. apply series_sum_wd. intros n. simpl. change ((([--][1])[^]n)[*]c[^](2*n)[=][--]([1][*]c[*]c)[^]n). rstepr ((([--][1])[*]c[*]c)[^]n). csetoid_rewrite_rev (nexp_mult _ c 2 n). csetoid_rewrite_rev (mult_nexp _ ([--][1]) (c[^]2) n). rational. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac