proposition: Lemma Is_refining_T_property:forall xi r1 r2, ((-1)<=r1<=1)%R->((-1)<=r2<=1)%R->Is_refining_T xi-> ((-1)<=as_Tensor xi r1 r2<=1)%R.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) r1 r2 H_r1 H_r2 H_refining. generalize (Is_refining_T_denom_nonvanishing_T _ _ _ H_refining H_r1 H_r2). generalize H_refining; intros [H_bounded _]. unfold denom_nonvanishing_T, as_Tensor, fst, snd. destruct (Is_refining_T_h_minusplus_efg_sign_dec _ _ _ _ _ _ _ _ H_refining) as [[H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]]]| [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]]]]; [ generalize (Is_refining_T_auxiliary_1 _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8) | generalize (Is_refining_T_auxiliary_2 _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8) ]; intros [H14 [H15 [H16 [H17 H18]]]] H_denom. assert (H_crd:0<e*r1*r2+f*r1+g*r2+h); [apply Bounded_T_pos with a b c d; trivial|]. split. stepl (-1/1); [|field; auto]; apply Rmult_Rdiv_pos_Rle; auto; apply Rle_zero_Rminus; stepr ((Qplus e a)*r1*r2+(Qplus f b)*r1+(Qplus g c)*r2+(Qplus h d)); [|realify_Q_goal; ring]; apply Bounded_T_auxiliary_5; trivial; [ring_exact_Q H1|ring_exact_Q H3|ring_exact_Q H5|ring_exact_Q H7]. stepr (1/1); [|field; auto]; apply Rmult_Rdiv_pos_Rle; auto; apply Rle_zero_Rminus; stepr ((Qminus e a)*r1*r2+(Qminus f b)*r1+(Qminus g c)*r2+(Qminus h d)); [|realify_Q_goal; ring]; apply Bounded_T_auxiliary_5; trivial; [ring_exact_Q H2|ring_exact_Q H4|ring_exact_Q H6|ring_exact_Q H8]. assert (H_crd:e*r1*r2+f*r1+g*r2+h<0); [apply Bounded_T_neg with a b c d; trivial|]. split. stepl (1/(-1)); [|field; auto]; apply Rmult_Rdiv_neg_Rle; auto; apply Rminus_le; stepl ((Qplus e a)*r1*r2+(Qplus f b)*r1+(Qplus g c)*r2+(Qplus h d)); [|realify_Q_goal; ring]. apply Bounded_T_auxiliary_6; trivial; [ring_exact_Q H1|ring_exact_Q H3|ring_exact_Q H5|ring_exact_Q H7]. stepr (-1/-1); [|field; auto]; apply Rmult_Rdiv_neg_Rle; auto; apply Rminus_le; stepl ((Qminus e a)*r1*r2+(Qminus f b)*r1+(Qminus g c)*r2+(Qminus h d)); [|realify_Q_goal; ring]; apply Bounded_T_auxiliary_6; trivial; [ring_exact_Q H2|ring_exact_Q H4|ring_exact_Q H6|ring_exact_Q H8]. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier