proposition: Lemma AQexp_neg_bounded_correct : ∀ (n : nat) a (abound : -1 ≤ a * (1 ≪ (-1)) ^ n ≤ 0), a ≤ 0 -> ' ARpower_2_iter n (AQexp_small_neg abound) = rational_exp (' a).
proof: Proof. induction n. - intros. simpl. rewrite AQexp_small_neg_correct. rewrite rational_exp_small_neg_correct. rewrite rational_exp_correct. apply CRIR.IRasCR_wd, Exponential.Exp_wd. apply Q_in_CReals.inj_Q_wd. rewrite rings.preserves_mult. unfold pow. simpl. rewrite rings.preserves_1, Qmult_1_r. reflexivity. - intros a abound aneg. change (ARpower_2_iter (S n) (AQexp_small_neg abound)) with (ARpower_N_bounded 2 1 (ARcompress (ARpower_2_iter n (AQexp_small_neg abound)))). rewrite ARcompress_correct. rewrite ARtoCR_preserves_power_N_bounded. assert (-1 ≤ a * (1 ≪ (-1)) * (1 ≪ (-1)) ^ n ≤ 0) as abound_shift. { setoid_replace (a * 1 ≪ (-1) * (1 ≪ (-1)) ^ n ) with (a * (1 ≪ (-1)) ^ S n). exact abound. unfold pow at 2. simpl. rewrite (rings.mult_assoc a). reflexivity. } specialize (IHn _ abound_shift). setoid_replace (' ARpower_2_iter n (AQexp_small_neg abound)) with (' ARpower_2_iter n (AQexp_small_neg abound_shift)). rewrite IHn. clear IHn. transitivity (CRpower_N_bounded 2 (1#1)%Qpos (rational_exp (' (a ≪ (-1))))). + apply Cmap_wd. setoid_replace ('1 : Qpos) with (1#1)%Qpos. reflexivity. rewrite AQposAsQpos_preserves_1. reflexivity. setoid_replace (' (a * 1 ≪ (-1))) with (' (a ≪ (-1))). reflexivity. rewrite aq_shift_opp_1. rewrite rings.preserves_mult. rewrite aq_shift_opp_1. apply Qmult_comp. reflexivity. rewrite rings.preserves_1. reflexivity. + rewrite aq_shift_opp_1. apply rational_exp_square. now apply semirings.preserves_nonpos. + apply (order_reflecting (cast AQ Q)). rewrite rings.preserves_mult. rewrite rings.preserves_0. rewrite <- (Qmult_0_l (' (1 ≪ (-1)))). apply Qmult_le_compat_r. apply (order_preserving (cast AQ Q)) in aneg. rewrite rings.preserves_0 in aneg. exact aneg. rewrite aq_shift_opp_1. rewrite rings.preserves_1. discriminate. + apply ARpower_2_iter_wd. apply (injective (cast AR CR)). rewrite AQexp_small_neg_correct, AQexp_small_neg_correct. apply rational_exp_small_neg_wd. setoid_replace (' (a * (1 ≪ (-1)) ^ S n)) with (' (a * 1 ≪ (-1) * (1 ≪ (-1)) ^ n)). reflexivity. unfold pow at 1. simpl. rewrite (rings.mult_assoc a). reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program MathClasses.misc.workaround_tactics CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith