proposition: Lemma upper_bound_Tensor_Moebius_Q_r:forall xi (H_xi:Is_refining_T xi), {q | Zero < q /\ (forall x1 x2 y (Hx1:-Qone<=x1/\x1<=Qone) (Hx2:-Qone<=x2/\x2<=Qone) (Hy:-Qone<=y/\y<=Qone), Zero < Qabs (x1-x2) -> Qabs ((as_Tensor_Q xi x1 y)-(as_Tensor_Q xi x2 y)) < q*(Qabs (x1-x2)))}.
proof: Proof. intros xi H_xi. destruct (upper_bound_Tensor_Moebius_Q_r_eta_discriminant xi H_xi) as [Y [H_Y1 H_Y2]]. destruct (upper_bound_Tensor_Moebius_Q_r_determinant xi H_xi) as [W [H_W1 H_W2]]. exists (Y*W); split; auto. intros x1 x2 y Hx1 Hx2 Hy Hx12. rewrite (upper_bound_Tensor_Moebius_Q_r_relative xi H_xi _ _ _ Hx1 Hx2 Hy). stepr ((Qabs (x1-x2)) *(W* Y)); [|ring]. stepl (Qabs (x1 - x2) * ( Qabs (Determinant (Tensor_Moebius_Q_r xi y)) * (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)))); [|ring]. apply Qlt_reg_mult_pos_l; trivial. apply Qmult_Qlt_Qle_nonneg_pos_compat; trivial. apply H_W2; assumption. apply H_Y2; assumption. apply Qabs_nonneg. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M