proposition: Lemma upper_bound_Tensor_Moebius_Q_l:forall xi (H_xi:Is_refining_T xi), {q | Zero < q /\ (forall x y1 y2 (Hx:-Qone<=x/\x<=Qone) (Hy1:-Qone<=y1/\y1<=Qone)(Hy2:-Qone<=y2/\y2<=Qone), Zero < Qabs (y1-y2) -> Qabs ((as_Tensor_Q xi x y1)-(as_Tensor_Q xi x y2)) < q*(Qabs (y1-y2)))}.
proof: Proof. intros xi H_xi. destruct (upper_bound_Tensor_Moebius_Q_l_eta_discriminant xi H_xi) as [Y [H_Y1 H_Y2]]. destruct (upper_bound_Tensor_Moebius_Q_l_determinant xi H_xi) as [W [H_W1 H_W2]]. exists (Y*W); split; auto. intros x y1 y2 Hx Hy1 Hy2 Hy12. rewrite (upper_bound_Tensor_Moebius_Q_l_relative xi H_xi _ _ _ Hx Hy1 Hy2). stepr ((Qabs (y1-y2)) *(W* Y)); [|ring]. stepl (Qabs (y1 - y2) * ( Qabs (Determinant (Tensor_Moebius_Q_l xi x)) * (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)))); [|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