proposition: Theorem thesis_5_6_10':forall xi alpha beta, Is_refining_T xi->{n:nat & {d| Incl_T (product_init_zip xi alpha beta n) d}}.
proof: Proof. intros xi alpha beta H_refining. destruct (thesis_5_6_19 redundancy xi H_refining redundancy_pos) as [theta1 [theta2 [H1 [H2 H_theta]]]]. set (q1:=(2/theta1)). set (q2:=(2/theta2)). destruct (Q_Archimedean_nat_inf q1) as [n1 Hn1]. destruct (Q_Archimedean_nat_inf q2) as [n2 Hn2]. set (n:=Max.max n1 n2). assert (Hnn1:=Max.le_max_l n1 n2: (n1<=n)%nat). assert (Hnn2:=Max.le_max_r n1 n2: (n2<=n)%nat). assert (H_mu_l:=Is_refining_M_product_init_pure alpha n). assert (H_mu_r:=Is_refining_M_product_init_pure beta n). assert (H_prod:=Is_refining_T_left_right_product _ _ _ H_refining H_mu_l H_mu_r). exists n. generalize (ub_is_in_base_interval n alpha). generalize (lb_is_in_base_interval n alpha). generalize (ub_is_in_base_interval n beta). generalize (lb_is_in_base_interval n beta). set (u1:=ub alpha n). set (l1:=lb alpha n). set (u2:=ub beta n). set (l2:=lb beta n). intros H_l2 H_u2 H_l1 H_u1. assert (H_ul1':Qabs (u1 - l1) < theta1). unfold u1,l1; rewrite Qabs_eq_pos; [|apply Qlt_Qminus_Zero; apply lb_lt_ub_pointwise]; apply Qle_lt_trans with (2%nat / (n + 1%nat)); [apply thesis_5_7_9|]; stepl (2/(n + 1%nat)); trivial; apply Qle_lt_trans with (2/(n1 + 1%nat)). let t_local:=natq_zero; apply Z_to_Qlt; apply inj_lt; auto with arith in apply Qmult_Qdiv_pos_Qle; [natq_S n; t_local|natq_S n1; t_local| ]; apply Qle_Zero_Qminus; qnat_S n; qnat_S n1; stepr (2*(n-n1)); [|ring]; apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; apply Z_to_Qle; apply inj_le; trivial. revert Hn1; unfold q1; intros Hn1; apply Qmult_pos_Qdiv_Qlt; [| rewrite Qmult_sym; stepl (2*Qone); [|ring]; apply Qdiv_Qmult_pos; auto; stepr (n1 + 1%nat); [|field; auto]; apply Qle_lt_trans with n1; trivial ]; natq_S n1; natq_zero; apply Z_to_Qlt; apply inj_lt; auto with arith. assert (H_ul1:Qabs (l1 - u1) < theta1);[rewrite Qabs_Qopp; stepl (Qabs (u1-l1)); trivial; apply (f_equal Qabs); ring|]. assert (H_ul2':Qabs (u2 - l2) < theta2). unfold u2,l2; rewrite Qabs_eq_pos; [|apply Qlt_Qminus_Zero; apply lb_lt_ub_pointwise]; apply Qle_lt_trans with (2%nat / (n + 1%nat)); [apply thesis_5_7_9|]; stepl (2/(n + 1%nat)); trivial; apply Qle_lt_trans with (2/(n2 + 1%nat)). let t_local:=natq_zero; apply Z_to_Qlt; apply inj_lt; auto with arith in apply Qmult_Qdiv_pos_Qle; [natq_S n; t_local|natq_S n2; t_local| ]; apply Qle_Zero_Qminus; qnat_S n; qnat_S n1; stepr (2*(n-n2)); [|ring]; apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; apply Z_to_Qle; apply inj_le; trivial. revert Hn2; unfold q1; intros Hn2; apply Qmult_pos_Qdiv_Qlt; [| rewrite Qmult_sym; stepl (2*Qone); [|ring]; apply Qdiv_Qmult_pos; auto; stepr (n2 + 1%nat); [|field; auto]; apply Qle_lt_trans with n2; trivial ]; natq_S n2; natq_zero; apply Z_to_Qlt; apply inj_lt; auto with arith. assert (H_ul2:Qabs (l2 - u2) < theta2);[rewrite Qabs_Qopp; stepl (Qabs (u2-l2)); trivial; apply (f_equal Qabs); ring|]. generalize (H_theta l1 l2 u1 u2 H_l1 H_l2 H_u1 H_u2 H_ul1 H_ul2). revert H_l2 H_u2 H_l1 H_u1; unfold u1,l1,u2,l2; repeat rewrite <- product_init_pure_ub; repeat rewrite <- product_init_pure_lb; intros H_l2 H_u2 H_l1 H_u1. rewrite <- (diameter2_product _ _ _ H_refining H_prod H_mu_l H_mu_r H_l1 H_l2 H_u1 H_u2). intros H_diam. destruct (thesis_5_6_20 _ _ H_diam) as [d Hd]. exists d. rewrite product_init_zip_product_init_pure; assumption. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M