proposition: Lemma upper_bound_Tensor_Moebius_Q_l_relative: forall xi (H_xi:Is_refining_T xi) x y1 y2, -Qone<=x/\x<=Qone -> -Qone<=y1/\y1<=Qone -> -Qone<=y2/\y2<=Qone -> Qabs ((as_Tensor_Q xi x y1)-(as_Tensor_Q xi x y2)) = (Qabs (Determinant (Tensor_Moebius_Q_l xi x))) * (Qabs (y1-y2)) * (Qabs(as_Moebius_Q (eta_discriminant (Tensor_Moebius_Q_l xi x)) y1) *Qabs(as_Moebius_Q (eta_discriminant (Tensor_Moebius_Q_l xi x)) y2)).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) [H_bound _] x y1 y2 [Hxl Hxu] [Hy1l Hy1u] [Hy2l Hy2u]; assert (H_denom1:e * x * y1 + f * x + g * y1 + 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 * x * y2 + f * x + g * y2 + 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_l, 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