proposition: Lemma upper_bound_Tensor_Moebius_Q_r_determinant: forall xi (H_xi:Is_refining_T xi), { W : Q | Zero < W /\ forall y, -Qone<=y/\y<=Qone -> Qabs (Determinant (Tensor_Moebius_Q_r xi y))< W }.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_xi. unfold Determinant, Tensor_Moebius_Q_r, fst, snd. set (W1 := Qmax4 ((Qabs (a*g)) + Qabs (a*h+g*b) + b*h) (-(Qabs (a*g)) + -Qabs (a*h+g*b) + b*h) (-(Qabs (c*e)) + -Qabs (c*f+e*d) + d*f) ((Qabs (c*e)) + Qabs (c*f+e*d) + d*f)). set (W2 := Qmin4 ((Qabs (a*g)) + Qabs (a*h+g*b) + b*h) (-(Qabs (a*g)) + -Qabs (a*h+g*b) + b*h) (-(Qabs (c*e)) + -Qabs (c*f+e*d) + d*f) ((Qabs (c*e)) + Qabs (c*f+e*d) + d*f)). exists ((W1-W2)+Qone); split. apply Qle_lt_reg_pos; auto; apply Qle_Qminus_Zero; subst W1 W2; apply Qmin4_Qmax4_Qle. intros y [Hyl Hyu]. apply Qle_lt_trans with (W1-W2); [|apply Qlt_Zero_Qminus; stepr Qone; auto; ring]. apply Qabs_Qminus_bound; unfold W1,W2. apply Qle_trans with (-(Qabs (a*g)) + -Qabs (a*h+g*b) + b*h); [apply Qle_Qmin4_2| apply (lower_bound_affine_base_interval_twice a b g h); assumption]. apply Qle_trans with ((Qabs (a*g)) + Qabs (a*h+g*b) + b*h); [apply (upper_bound_affine_base_interval_twice a b g h); assumption|apply Qle_Qmax4_1]. apply Qle_trans with (-(Qabs (c*e)) + -Qabs (c*f+e*d) + d*f); [apply Qle_Qmin4_3| apply (lower_bound_affine_base_interval_twice c d e f); assumption]. apply Qle_trans with ((Qabs (c*e)) + Qabs (c*f+e*d) + d*f); [apply (upper_bound_affine_base_interval_twice c d e f); assumption|apply Qle_Qmax4_4]. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M