proposition: Lemma Is_refining_T_emits_q_pointwise: forall n xi alpha beta H_r, let smodu:=semantic_modulus_q xi alpha beta H_r in n = projT1 smodu -> emits_q xi alpha beta.
proof: Proof. induction n; intros xi alpha beta H_r smodu Hn; set (n':=projS1 smodu); set (d:=(proj1_sig (projT2 smodu))); assert (Hn':n'=(projT1 smodu)); trivial; assert (Hd:d=(proj1_sig (projT2 smodu))); trivial; destruct (proj2_sig (projT2 smodu)) as [H1 H3]. simpl in H1. case (Incl_T_dec_D xi LL); intros t_l. constructor 1; trivial. case (Incl_T_dec_D xi RR); intros t_r. constructor 2; trivial. case (Incl_T_dec_D xi MM); intros t_m. constructor 3; trivial. rewrite_all <- Hd; rewrite_all <- Hn'; rewrite_all <- Hn; destruct d; contradiction. rewrite_all <- Hd; rewrite_all <- Hn. generalize (H3 O LL (lt_O_Sn _)); generalize (H3 O RR (lt_O_Sn _)); generalize (H3 O MM (lt_O_Sn _)). simpl; intros t_m t_r t_l. constructor 4; trivial. apply (IHn (right_product (left_product xi (hd alpha)) (hd beta)) (tl alpha) (tl beta) (Is_refining_T_product_hd _ _ _ H_r)). apply eq_add_S. apply (semantic_modulus_q_S_product (S n) (projT1 (semantic_modulus_q (right_product (left_product xi (hd alpha)) (hd beta)) (tl alpha) (tl beta) (Is_refining_T_product_hd _ _ _ H_r))) xi alpha beta H_r (Is_refining_T_product_hd _ _ _ H_r)); trivial. apply lt_O_Sn. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M