Various properties of ArcTangent.
Lemma Dom_Tang_ArcTan : forall x, (Dom Tang (ArcTan x)).
Lemma ArcTan_zero : ArcTan 0[=]0.
Lemma ArcTan_one : ArcTan 1[=]π[/]4.
Lemma ArcTan_inv : forall x, ArcTan [--]x[=][--](ArcTan x).
Lemma ArcTan_resp_less : forall x y, x[<]y -> ArcTan x[<]ArcTan y.
Lemma ArcTan_resp_leEq : forall x y, x[<=]y -> ArcTan x[<=]ArcTan y.
Lemma ArcTan_pos : forall x, 0[<]x -> 0[<]ArcTan x.
Lemma ArcTan_recip : forall x Hx, 0[<]x -> ArcTan (1[/]x[//]Hx)[=]π[/]2[-](ArcTan x).
Lemma ArcTan_plus_ArcTan : forall x y Hxy,
([--]1[<=]x) -> (x[<=]1) -> ([--]1[<=]y) -> (y[<=]1) ->
ArcTan x [+] ArcTan y [=] ArcTan ((x[+]y)[/](1[-]x[*]y)[//]Hxy).
Section ArcTan_Series.
ArcTan Series
In this section we show the convergence of ArcTan's power series.First we show the convergence of the series for 1/(1+x^2)
Lemma bellcurve_series_convergent_IR : fun_series_convergent_IR ((⋅,⋅) ([--]1) 1) (fun (i:nat) => ([--]1)[^]i{**}Fid IR{^}(2*i)).
Lemma bellcurve_series
: forall (Hs:fun_series_convergent_IR ((⋅,⋅) ([--]1) 1) (fun (i:nat) => ([--]1)[^]i{**}Fid IR{^}(2*i))),
≈ ((⋅,⋅) ([--]1) 1) (∑'∞ Hs) ({1/}([-C-]1{+}FId{^}2)).
Finally we show the convergence of the series for arctan.
Lemma arctan_series_convergent_IR : fun_series_convergent_IR ((⋅,⋅) ([--]1) 1)
(fun (i:nat) => (([--]1)[^]i[/]nring (S (2*i))[//]nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1)).
Lemma arctan_series : forall c : IR,
forall (Hs:fun_series_convergent_IR ((⋅,⋅) ([--]1) 1) (fun (i:nat) => (([--]1)[^]i[/]nring (S (2*i))[//]nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1))) Hc,
∑'∞ Hs c Hc[=]ArcTan c.
End ArcTan_Series.