proposition: Lemma upper_bound_Tensor_Moebius_Q_l_determinant: forall xi (H_xi:Is_refining_T xi), { W : Q | Zero < W /\ forall x, -Qone<=x/\x<=Qone -> Qabs (Determinant (Tensor_Moebius_Q_l xi x))< W }.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_xi. unfold Determinant, Tensor_Moebius_Q_l, fst, snd. set (W1 := Qmax4 ((Qabs (a*f)) + Qabs (a*h+f*c) + c*h) (-(Qabs (a*f)) + -Qabs (a*h+f*c) + c*h) (-(Qabs (b*e)) + -Qabs (b*g+e*d) + d*g) ((Qabs (b*e)) + Qabs (b*g+e*d) + d*g)). set (W2 := Qmin4 ((Qabs (a*f)) + Qabs (a*h+f*c) + c*h) (-(Qabs (a*f)) + -Qabs (a*h+f*c) + c*h) (-(Qabs (b*e)) + -Qabs (b*g+e*d) + d*g) ((Qabs (b*e)) + Qabs (b*g+e*d) + d*g)). exists ((W1-W2)+Qone); split. apply Qle_lt_reg_pos; auto; apply Qle_Qminus_Zero; subst W1 W2; apply Qmin4_Qmax4_Qle. intros x [Hxl Hxu]. 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*f) + -Qabs (a*h+f*c) + c*h); [apply Qle_Qmin4_2| apply (lower_bound_affine_base_interval_twice a c f h); assumption]. apply Qle_trans with ( Qabs (a*f) + Qabs (a*h+f*c) + c*h); [apply (upper_bound_affine_base_interval_twice a c f h); assumption|apply Qle_Qmax4_1]. apply Qle_trans with (-(Qabs (b*e)) + -Qabs (b*g+e*d) + d*g); [apply Qle_Qmin4_3| apply (lower_bound_affine_base_interval_twice b d e g); assumption]. apply Qle_trans with ((Qabs (b*e)) + Qabs (b*g+e*d) + d*g); [apply (upper_bound_affine_base_interval_twice b d e g); 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