Arctangent

Using pi and properties of arctangent, we define arctangent from 1 to infinity.
Definition rational_arctan_big_pos (a:Q) (Ha:1 <= a) : CR.
Defined.

Lemma rational_arctan_big_pos_correct : forall a (Ha: 1 <= a), 1 < a ->
 (rational_arctan_big_pos Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.

Because we have slow convergence near 1, we have another compuation that works for nonnegative numbers, and is particularly fast near 1.
Definition rational_arctan_mid_pos (a:Q) (Ha:0 <= a) : CR.

Lemma rational_arctan_mid_pos_correct : forall a (Ha: 0 <= a), 0 < a ->
 (rational_arctan_mid_pos Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.

We glue all of are different methods of computing arctangent into a nice fast one that works for nonnegative numbers.
Definition rational_arctan_pos (a:Q) (Ha:0 <= a) : CR.
Defined.

Lemma rational_arctan_pos_correct : forall a (Ha: 0 <= a),
 (rational_arctan_pos Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.

By symmetry we get arctangent for all numbers.
Definition rational_arctan (a:Q) : CR.
Defined.

Lemma rational_arctan_correct : forall (a:Q),
 (rational_arctan a == IRasCR (ArcTan (inj_Q IR a)))%CR.

Lift arctangent on the rationals to the reals.
Lemma arctan_uc_prf : is_UniformlyContinuousFunction rational_arctan Qpos2QposInf.

Definition arctan_uc : Q_as_MetricSpace --> CR :=
Build_UniformlyContinuousFunction arctan_uc_prf.

Definition arctan : CR --> CR := Cbind QPrelengthSpace arctan_uc.

Lemma arctan_correct : forall x,
 (IRasCR (ArcTan x) == arctan (IRasCR x))%CR.
Lemma arctan_Qarctan : forall x : Q, (arctan (' x) == rational_arctan x)%CR.