proposition: Lemma upper_bound_Tensor_Moebius_Q_r_relative: forall xi (H_xi:Is_refining_T xi) x1 x2 y, -Qone<=x1/\x1<=Qone -> -Qone<=x2/\x2<=Qone -> -Qone<=y/\y<=Qone -> Qabs ((as_Tensor_Q xi x1 y)-(as_Tensor_Q xi x2 y)) = (Qabs (Determinant (Tensor_Moebius_Q_r xi y))) * (Qabs (x1-x2)) * (Qabs(as_Moebius_Q (eta_discriminant (Tensor_Moebius_Q_r xi y)) x1) *Qabs(as_Moebius_Q (eta_discriminant (Tensor_Moebius_Q_r xi y)) x2)).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) [H_bound _] x1 x2 y [Hx1l Hx1u] [Hx2l Hx2u] [Hyl Hyu]; assert (H_denom1:e * x1 * y + f * x1 + g * y + h <> Zero); [apply Q_to_R_Qneq; realify_Q; intros; apply Bounded_T_nonzero_denum with a b c d; trivial; split; trivial|]; assert (H_denom2:e * x2 * y + f * x2 + g * y + h <> Zero); [apply Q_to_R_Qneq; realify_Q; intros; apply Bounded_T_nonzero_denum with a b c d; trivial; split; trivial|]; unfold as_Tensor_Q, Tensor_Moebius_Q_r, as_Moebius_Q, eta_discriminant, Determinant, fst, snd; qZ_numerals; repeat rewrite <- Qabs_Qmult; repeat rewrite Qminus_Qdiv; trivial; apply (f_equal Qabs); field; repeat split; auto; [ring_exact_Q H_denom2|ring_exact_Q H_denom1]. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M