proposition: Lemma as_Tensor_L: forall xi r1 r2, denom_nonvanishing_T xi r1 r2 -> ((-1)<=as_Tensor xi r1 r2<=1)%R-> as_Tensor (m_product LL xi) r1 r2 = ((as_Tensor xi r1 r2 - 1) / (as_Tensor xi r1 r2 + 3))%R.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) r1 r2 H_denom H_r. generalize (denom_nonvanishing_T_m_product _ _ _ _ Is_refining_M_L H_r H_denom); generalize H_denom; clear H_denom H_r. unfold m_product, as_Tensor, denom_nonvanishing_M, denom_nonvanishing_T, map_digits, fst, snd. realify_Q ;auto; simpl. replace (2+1) with 3; [|ring]. intros H_denom H_denom_product. assert (H_denom':a*r1*r2+b*r1+c*r2+d+(e*r1*r2+f*r1+g*r2+h)*3<>0); [ apply Rmult_reg_nonzero_l with (1/2); stepl ((1/2*a+3/2*e)*r1*r2+(1/2*b+3/2*f)*r1+(1/2*c+3/2*g)*r2+(1/2*d+3/2*h)); trivial; field; auto|]. rewrite Rdiv_Rminus_Rmult; trivial. rewrite Rdiv_Rplus_Rmult; trivial. rewrite Rdiv_Rdiv_simplify; trivial. transitivity(((a*r1*r2+b*r1+c*r2+d-(e*r1*r2+f*r1+g*r2+h)*1)*(1/2))/((a*r1*r2+b*r1+c*r2+d+(e*r1*r2+f*r1+g*r2+h)*3)*(1/2))). apply (f_equal2 Rdiv); field; auto. apply Rdiv_Rmult_simplify; auto. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier