proposition: Lemma Is_refining_M_Bounded_M_product:forall mu mu',Is_refining_M mu' -> Bounded_M mu -> Bounded_M (product mu mu').
proof: Proof. intros ((a,b),(c,d)) ((a',b'),(c',d')) H_refining' H_bounded. apply denom_nonvanishing_M_Bounded_M; intros r Hr. assert (H_mu':=Is_refining_M_property _ r Hr H_refining'). generalize (Bounded_M_denom_nonvanishing_M _ H_bounded _ H_mu'). unfold as_Moebius, denom_nonvanishing_M, product, fst, snd. intros H_denom. repeat rewrite Q_to_Rplus; repeat rewrite Q_to_Rmult. stepl (c*(a'*r+b')+d*(c'*r+d')); [|ring]. apply Rlinear_non_zero_2; auto. apply (Is_refining_M_denom_nonvanishing_M _ _ H_refining' Hr). Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M