Arctangent (small)
For values between in [0,1], arctangent is computed by it's alternating taylor series.
Section ArcTanSeries.
Variable a:Q.
Definition arctanSequence := (mult_Streams (everyOther recip_positives) (powers_help (a^2) a)).
Lemma Str_nth_arctanSequence : forall n, (Str_nth n arctanSequence == (1#P_of_succ_nat (2*n))*a^(1+2*n)%nat)%Q.
Hypothesis Ha: 0 <= a <= 1.
Lemma square_zero_one : 0 <= a^2 <= 1.
Lemma arctanSequence_dnn : DecreasingNonNegative arctanSequence.
Lemma arctanSequence_zl : Limit arctanSequence 0.
End ArcTanSeries.
Definition rational_arctan_small_pos (a:Q) (p: 0 <= a <= 1) : CR :=
InfiniteAlternatingSum (arctanSequence_dnn p) (arctanSequence_zl p).
Lemma rational_arctan_small_pos_correct : forall (a:Q) Ha, a < 1 ->
(@rational_arctan_small_pos a Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.
Variable a:Q.
Definition arctanSequence := (mult_Streams (everyOther recip_positives) (powers_help (a^2) a)).
Lemma Str_nth_arctanSequence : forall n, (Str_nth n arctanSequence == (1#P_of_succ_nat (2*n))*a^(1+2*n)%nat)%Q.
Hypothesis Ha: 0 <= a <= 1.
Lemma square_zero_one : 0 <= a^2 <= 1.
Lemma arctanSequence_dnn : DecreasingNonNegative arctanSequence.
Lemma arctanSequence_zl : Limit arctanSequence 0.
End ArcTanSeries.
Definition rational_arctan_small_pos (a:Q) (p: 0 <= a <= 1) : CR :=
InfiniteAlternatingSum (arctanSequence_dnn p) (arctanSequence_zl p).
Lemma rational_arctan_small_pos_correct : forall (a:Q) Ha, a < 1 ->
(@rational_arctan_small_pos a Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.
Extend the range to [-1,1] by symmetry.
Definition rational_arctan_small (a:Q) (p: -(1) <= a <= 1) : CR.
Defined.
Lemma rational_arctan_small_correct : forall (a:Q) Ha, -(1) < a -> a < 1 ->
(@rational_arctan_small a Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.
Defined.
Lemma rational_arctan_small_correct : forall (a:Q) Ha, -(1) < a -> a < 1 ->
(@rational_arctan_small a Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.