proposition: Lemma Is_refining_T_property_fold: forall xi, (forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> denom_nonvanishing_T xi r1 r2) -> (forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> (-1<=as_Tensor xi r1 r2<=1)%R) -> Is_refining_T xi.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_denom H_xi. assert (H_bounded:=(denom_nonvanishing_T_Bounded_T _ H_denom)). unfold as_Tensor in H_xi; simpl in H_xi. assert (H_efgh1:=Bounded_T_e_mf_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh2:=Bounded_T_me_mf_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh3:=Bounded_T_me_f_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh4:=Bounded_T_e_f_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_h:=Bounded_T_nonzero _ _ _ _ _ _ _ _ H_bounded). unfold Is_refining_T, map_digits, fst, snd; qZ_numerals; repeat split; trivial. destruct (denom_nonvanishing_T_Bounded_T (((a,b),(c,d)),((e,f),(g,h))) H_denom) as [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]]; simpl in H1, H2, H3, H4. left; repeat split. apply Qle_Qdiv_denom_pos_nonneg with (e+f+g+h); trivial; stepr (((a*Qone*Qone+b*Qone+c*Qone+d)/(e*Qone*Qone+f*Qone+g*Qone+h))-(-Qone)); [|field; ring_exact_Q H_efgh4]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh4]. apply Qle_Qdiv_denom_pos_nonneg with (e+f+g+h); trivial; stepr (Qone -((a*Qone*Qone+b*Qone+c*Qone+d)/(e*Qone*Qone+f*Qone+g*Qone+h))); [|field; ring_exact_Q H_efgh4]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh4]. apply Qle_Qdiv_denom_pos_nonneg with (e-f-g+h); trivial; stepr (((a*(-Qone)*(-Qone)+b*(-Qone)+c*(-Qone)+d)/(e*(-Qone)*(-Qone)+f*(-Qone)+g*(-Qone)+h))-(-Qone)); [|field; ring_exact_Q H_efgh1]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh1]. apply Qle_Qdiv_denom_pos_nonneg with (e-f-g+h); trivial; stepr (Qone-((a*(-Qone)*(-Qone)+b*(-Qone)+c*(-Qone)+d)/(e*(-Qone)*(-Qone)+f*(-Qone)+g*(-Qone)+h))); [|field; ring_exact_Q H_efgh1]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh1]. apply Qle_Qdiv_denom_pos_nonneg with (-e-f+g+h); trivial; stepr (((a*(-Qone)*Qone+b*(-Qone)+c*Qone+d)/(e*(-Qone)*Qone+f*(-Qone)+g*Qone+h))-(-Qone)); [|field; ring_exact_Q H_efgh2]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh2]. apply Qle_Qdiv_denom_pos_nonneg with (-e-f+g+h); trivial; stepr (Qone-((a*(-Qone)*Qone+b*(-Qone)+c*Qone+d)/(e*(-Qone)*Qone+f*(-Qone)+g*Qone+h))); [|field; ring_exact_Q H_efgh2]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh2]. apply Qle_Qdiv_denom_pos_nonneg with (-e+f-g+h); trivial; stepr (((a*Qone*(-Qone)+b*Qone+c*(-Qone)+d)/(e*Qone*(-Qone)+f*Qone+g*(-Qone)+h))-(-Qone)); [|field; ring_exact_Q H_efgh3]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh3]. apply Qle_Qdiv_denom_pos_nonneg with (-e+f-g+h); trivial; stepr (Qone-((a*Qone*(-Qone)+b*Qone+c*(-Qone)+d)/(e*Qone*(-Qone)+f*Qone+g*(-Qone)+h))); [|field; ring_exact_Q H_efgh3]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh3]. right; repeat split. apply Qle_Qdiv_denom_neg_nonneg with (e+f+g+h); trivial; stepr (((a*Qone*Qone+b*Qone+c*Qone+d)/(e*Qone*Qone+f*Qone+g*Qone+h))-(-Qone)); [|field; ring_exact_Q H_efgh4]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh4]. apply Qle_Qdiv_denom_neg_nonneg with (e+f+g+h); trivial; stepr (Qone -((a*Qone*Qone+b*Qone+c*Qone+d)/(e*Qone*Qone+f*Qone+g*Qone+h))); [|field; ring_exact_Q H_efgh4]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh4]. apply Qle_Qdiv_denom_neg_nonneg with (e-f-g+h); trivial; stepr (((a*(-Qone)*(-Qone)+b*(-Qone)+c*(-Qone)+d)/(e*(-Qone)*(-Qone)+f*(-Qone)+g*(-Qone)+h))-(-Qone)); [|field; ring_exact_Q H_efgh1]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh1]. apply Qle_Qdiv_denom_neg_nonneg with (e-f-g+h); trivial; stepr (Qone-((a*(-Qone)*(-Qone)+b*(-Qone)+c*(-Qone)+d)/(e*(-Qone)*(-Qone)+f*(-Qone)+g*(-Qone)+h))); [|field; ring_exact_Q H_efgh1]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh1]. apply Qle_Qdiv_denom_neg_nonneg with (-e-f+g+h); trivial; stepr (((a*(-Qone)*Qone+b*(-Qone)+c*Qone+d)/(e*(-Qone)*Qone+f*(-Qone)+g*Qone+h))-(-Qone)); [|field; ring_exact_Q H_efgh2]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh2]. apply Qle_Qdiv_denom_neg_nonneg with (-e-f+g+h); trivial; stepr (Qone-((a*(-Qone)*Qone+b*(-Qone)+c*Qone+d)/(e*(-Qone)*Qone+f*(-Qone)+g*Qone+h))); [|field; ring_exact_Q H_efgh2]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval))| ring_exact_Q H_efgh2]. apply Qle_Qdiv_denom_neg_nonneg with (-e+f-g+h); trivial; stepr (((a*Qone*(-Qone)+b*Qone+c*(-Qone)+d)/(e*Qone*(-Qone)+f*Qone+g*(-Qone)+h))-(-Qone)); [|field; ring_exact_Q H_efgh3]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj1 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh3]. apply Qle_Qdiv_denom_neg_nonneg with (-e+f-g+h); trivial; stepr (Qone-((a*Qone*(-Qone)+b*Qone+c*(-Qone)+d)/(e*Qone*(-Qone)+f*Qone+g*(-Qone)+h))); [|field; ring_exact_Q H_efgh3]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; [ apply (proj2 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval))| ring_exact_Q H_efgh3]. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier