proposition: Lemma upper_bound_Tensor_Moebius_Q_r_eta_discriminant: forall xi (H_xi:Is_refining_T xi), { Y:Q | Zero < Y /\ (forall x1 x2 y, -Qone<=x1/\x1<=Qone -> -Qone<=x2/\x2<=Qone -> -Qone<=y/\y<=Qone -> 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)<= Y)}.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_xi. assert (H_bounded:=proj1 H_xi); assert (H1:=Bounded_T_e_mf_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H2:=Bounded_T_me_mf_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H3:=Bounded_T_me_f_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H4:=Bounded_T_e_f_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded). unfold Determinant, Tensor_Moebius_Q_r, eta_discriminant, as_Moebius_Q, fst, snd. set (Y:=Qmax4 (Qabs (Qone/(e+f+g+h))) (Qabs (Qone/(-e-f+g+h))) (Qabs (Qone/(-e+f-g+h))) (Qabs (Qone/(e-f-g+h)))). exists (Y*Y); split; subst Y. apply Qmult_mult_pos; apply Qlt_not_eq; apply Qmax4_Qlt_upper_bound; apply Qabs_nonzero_pos; apply Qinv_resp_nonzero_Qdiv; [ring_exact_Q H4|ring_exact_Q H2|ring_exact_Q H3|ring_exact_Q H1]. intros x1 x2 y Hx1 Hx2 Hy. assert (Hy_lr:(-1<= y <= 1 )%R); [destruct Hy; realify_Q; intros; split; trivial|]. assert (H_by:=Bounded_T_M_r _ _ _ _ _ _ _ _ H_bounded y Hy). assert (H_b1:=Bounded_T_M_2 _ _ _ _ _ _ _ _ H_bounded). assert (H_b2:=Bounded_T_M_1 _ _ _ _ _ _ _ _ H_bounded). assert (H_b2':Bounded_M (-a+c,-b+d,(-e+g,-f+h))); [ replace (-a+c) with (c-a); [|ring]; replace (-b+d) with (d-b); [|ring]; replace (-e+g) with (g-e); [|ring]; replace (-f+h) with (h-f); [|ring]; assumption|]. assert (H_dy1:e*y+f+(g*y+h)<>Zero); [generalize (Bounded_M_nonzero_denum _ _ _ _ y H_b1 Hy_lr); rationalify_R_goal; intros H_tmp; assert (H_:=Q_to_R_Qneq _ _ H_tmp); ring_exact_Q H_|]. assert (H_dy2:g*y+h-(e*y+f)<>Zero); [generalize (Bounded_M_nonzero_denum _ _ _ _ y H_b2 Hy_lr); rationalify_R_goal; intros H_tmp; assert (H_:=Q_to_R_Qneq _ _ H_tmp); ring_exact_Q H_|]. apply Qmult_Qle_compat; try apply Qabs_nonneg; apply Qle_trans with (Qmax (Qabs (Qone / (e * y + f + (g * y + h)))) (Qabs (Qone / (g * y + h - (e * y + f))))); [ stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e * y + f, g * y + h)) x1)); trivial; apply (maximum_eta_discriminant_base_interval _ _ _ _ x1 H_by (proj1 Hx1) (proj2 Hx1)) | | stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e * y + f, g * y + h)) x2)); trivial; apply (maximum_eta_discriminant_base_interval _ _ _ _ x2 H_by (proj1 Hx2) (proj2 Hx2)) | ]. apply Qmax_lub. apply Qle_trans with (Qmax (Qabs (Qone / (e + g + (f + h)))) (Qabs (Qone / (f + h - (e + g))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e + g, f + h)) y)). apply (maximum_eta_discriminant_base_interval (a+c) (b+d) (e+g) (f+h) y H_b1 (proj1 Hy) (proj2 Hy)). unfold as_Moebius_Q, fst, snd; apply (f_equal Qabs); qZ_numerals; field; split; auto. apply Qmax_lub. stepl (Qabs (Qone / (e + f + g + h)));[apply Qle_Qmax4_1|apply (f_equal Qabs); field; ring_exact_Q H4]. stepl (Qabs (Qone / (- e + f - g + h)));[apply Qle_Qmax4_3|apply (f_equal Qabs); field; ring_exact_Q H3]. apply Qle_trans with (Qmax (Qabs (Qone / (- e + g + (- f + h)))) (Qabs (Qone / (- f + h - (- e + g))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (-e + g, -f + h)) y)). apply (maximum_eta_discriminant_base_interval (-a+c) (-b+d) (-e+g) (-f+h) y H_b2' (proj1 Hy) (proj2 Hy)). unfold as_Moebius_Q, fst, snd; apply (f_equal Qabs); qZ_numerals; field; split; auto. apply Qmax_lub. stepl (Qabs (Qone / (-e - f +g + h)));[apply Qle_Qmax4_2|apply (f_equal Qabs); field; ring_exact_Q H2]. stepl (Qabs (Qone / (e - f - g + h)));[apply Qle_Qmax4_4|apply (f_equal Qabs); field; ring_exact_Q H1]. apply Qmax_lub. apply Qle_trans with (Qmax (Qabs (Qone / (e + g + (f + h)))) (Qabs (Qone / (f + h - (e + g))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e + g, f + h)) y)). apply (maximum_eta_discriminant_base_interval (a+c) (b+d) (e+g) (f+h) y H_b1 (proj1 Hy) (proj2 Hy)). unfold as_Moebius_Q, fst, snd; apply (f_equal Qabs); qZ_numerals; field; split; auto. apply Qmax_lub. stepl (Qabs (Qone / (e + f + g + h)));[apply Qle_Qmax4_1|apply (f_equal Qabs); field; ring_exact_Q H4]. stepl (Qabs (Qone / (- e + f - g + h)));[apply Qle_Qmax4_3|apply (f_equal Qabs); field; ring_exact_Q H3]. apply Qle_trans with (Qmax (Qabs (Qone / (- e + g + (- f + h)))) (Qabs (Qone / (- f + h - (- e + g))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (-e + g, -f + h)) y)). apply (maximum_eta_discriminant_base_interval (-a+c) (-b+d) (-e+g) (-f+h) y H_b2' (proj1 Hy) (proj2 Hy)). unfold as_Moebius_Q, fst, snd; apply (f_equal Qabs); qZ_numerals; field; split; auto. apply Qmax_lub. stepl (Qabs (Qone / (-e - f +g + h)));[apply Qle_Qmax4_2|apply (f_equal Qabs); field; ring_exact_Q H2]. stepl (Qabs (Qone / (e - f - g + h)));[apply Qle_Qmax4_4|apply (f_equal Qabs); field; ring_exact_Q H1]. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M