proposition: Lemma AQsin_bounded_correct {n : nat} {num den : AQ} (Pnd : -(den * 3^n) ≤ num ≤ den * 3^n) (dpos : 0 < den * 3^n) : 'AQsin_bounded Pnd dpos = rational_sin ('num / 'den).
proof: Proof. revert num den dpos Pnd. induction n; intros. - unfold AQsin_bounded. simpl. rewrite AQsin_small_correct. change (3^0%nat) with 1. rewrite rings.mult_1_r. reflexivity. - unfold AQsin_bounded. change (' ucFun ARsin_poly (ARsin_poly_iter n (AQsin_small Pnd dpos)) = rational_sin (' num / ' den)). rewrite ARtoCR_preserves_sin_poly. unfold AQsin_bounded in IHn. assert (le (-(den * 3 * 3 ^ n)) num /\ num ≤ den * 3 * 3 ^ n) as H5. { rewrite <- (associativity den 3). exact Pnd. } assert (0 < den * 3 * 3 ^ n) as H6. { rewrite <- (associativity den 3). exact dpos. } setoid_replace (ARsin_poly_iter n (AQsin_small Pnd dpos)) with (ARsin_poly_iter n (AQsin_small H5 H6)). rewrite IHn. change (Qdiv ('num) ('(den * 3))) with (('num : Q) / '(den * 3)). rewrite rings.preserves_mult, rings.preserves_3. rewrite dec_fields.dec_recip_distr, associativity. apply rational_sin_poly. apply ARsin_poly_iter_wd. apply AQsin_small_pos_wd. reflexivity. rewrite <- (associativity den 3). reflexivity. Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith