proposition: Lemma product_init_rev_rep_drop_denom_nonvanishing: forall alpha n r d, rep alpha r -> Streams.hd (drop n alpha) = d -> (as_Moebius (map_digits d) (-1)<= as_Moebius (product_init_rev alpha n) r<= as_Moebius (map_digits d) 1)%R/\ rep (drop n alpha) (as_Moebius (product_init_rev alpha n) r)/\ denom_nonvanishing_M (product_init_rev alpha n) r.
proof: Proof. intros alpha n. generalize alpha; clear alpha; induction n. intros [[ | | ] alpha] r d Hr H_nth; unfold product_init_rev; simpl; unfold drop,Streams.hd in H_nth; subst d; [ rewrite as_Moebius_L_one; rewrite as_Moebius_L_min_one | rewrite as_Moebius_R_one; rewrite as_Moebius_R_min_one | rewrite as_Moebius_M_one; rewrite as_Moebius_M_min_one ]; unfold denom_nonvanishing_M, as_Moebius at 1 2 3, idM, fst, snd, Qdiv at 2 3 6 7; rewrite Qmult_zero; repeat rewrite Q_to_Rdiv; auto; repeat rewrite Q_to_R_Zero; repeat rewrite Z_to_Q_to_R_IZR; simpl; unfold Rdiv; repeat rewrite Rmult_0_l; rewrite Rplus_0_r; rewrite Rplus_0_l; rewrite Rmult_1_l; replace (/ 1 * r * / / 1)%R with r; try(field; auto); split; try (solve[split; auto]). apply (rep_L_inv_interval _ _ Hr). apply (rep_R_inv_interval _ _ Hr). apply (rep_M_inv_interval _ _ Hr). intros alpha r d Hr H_nth. unfold product_init_rev. rewrite rev_take_S_Str_nth; rewrite fold_right_cons. replace (fold_right product idM (rev (take n (Streams.map inv_digit alpha)))) with (product_init_rev alpha n); trivial. unfold map_reals; rewrite <- Str_nth_map_pointwise. generalize (drop_Str_nth n alpha). destruct (Str_nth n alpha); intros H_drop_n; destruct (IHn alpha _ _ Hr H_drop_n) as [[Hind1 Hind2] [Hind_rep H_denom]]. rewrite (hd_tl_id (drop n alpha)) in Hind_rep; rewrite H_drop_n in Hind_rep; rewrite <- (drop_tl_S n alpha) in Hind_rep; generalize (rep_L_inv _ _ Hind_rep); intros H_rep_Sn. rewrite as_Moebius_inv_L. split; [|split]; try exact (H_rep_Sn). rewrite (hd_tl_id (drop (S n) alpha)) in H_rep_Sn; rewrite H_nth in H_rep_Sn. destruct d. rewrite as_Moebius_L_min_one; rewrite as_Moebius_L_one; apply (rep_L_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_R_min_one; rewrite as_Moebius_R_one; apply (rep_R_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_M_min_one; rewrite as_Moebius_M_one; apply (rep_M_inv_interval _ _ H_rep_Sn)... apply denom_nonvanishing_M_product_inv_L. exact H_denom. rewrite <- as_Moebius_L_min_one; rewrite <- as_Moebius_L_one; split; trivial. exact H_denom. rewrite <- as_Moebius_L_min_one; rewrite <- as_Moebius_L_one; split; trivial. rewrite (hd_tl_id (drop n alpha)) in Hind_rep; rewrite H_drop_n in Hind_rep; rewrite <- (drop_tl_S n alpha) in Hind_rep; generalize (rep_R_inv _ _ Hind_rep); intros H_rep_Sn. rewrite as_Moebius_inv_R. split; [|split]; try exact (H_rep_Sn). rewrite (hd_tl_id (drop (S n) alpha)) in H_rep_Sn; rewrite H_nth in H_rep_Sn. destruct d. rewrite as_Moebius_L_min_one; rewrite as_Moebius_L_one; apply (rep_L_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_R_min_one; rewrite as_Moebius_R_one; apply (rep_R_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_M_min_one; rewrite as_Moebius_M_one; apply (rep_M_inv_interval _ _ H_rep_Sn)... apply denom_nonvanishing_M_product_inv_R. exact H_denom. rewrite <- as_Moebius_R_one; rewrite <- as_Moebius_R_min_one; split; trivial. exact H_denom. rewrite <- as_Moebius_R_one; rewrite <- as_Moebius_R_min_one; split; trivial. rewrite (hd_tl_id (drop n alpha)) in Hind_rep; rewrite H_drop_n in Hind_rep; rewrite <- (drop_tl_S n alpha) in Hind_rep; generalize (rep_M_inv _ _ Hind_rep); intros H_rep_Sn. rewrite as_Moebius_inv_M. split; [|split]; try exact (H_rep_Sn). rewrite (hd_tl_id (drop (S n) alpha)) in H_rep_Sn; rewrite H_nth in H_rep_Sn. destruct d. rewrite as_Moebius_L_min_one; rewrite as_Moebius_L_one; apply (rep_L_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_R_min_one; rewrite as_Moebius_R_one; apply (rep_R_inv_interval _ _ H_rep_Sn). rewrite as_Moebius_M_min_one; rewrite as_Moebius_M_one; apply (rep_M_inv_interval _ _ H_rep_Sn)... apply denom_nonvanishing_M_product_inv_M. exact H_denom. rewrite <- as_Moebius_M_one; rewrite <- as_Moebius_M_min_one; split; trivial. exact H_denom. rewrite <- as_Moebius_M_one; rewrite <- as_Moebius_M_min_one; split; trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs