proposition: Lemma upper_bound_Tensor_Moebius_Q_l_eta_discriminant: forall xi (H_xi:Is_refining_T xi), { Y:Q | Zero < Y /\ (forall x y1 y2, -Qone<=x/\x<=Qone -> -Qone<=y1/\y1<=Qone -> -Qone<=y2/\y2<=Qone -> 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)<= 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_l, 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 x y1 y2 Hx Hy1 Hy2. assert (Hx_lr:(-1<= x <= 1 )%R); [destruct Hx; realify_Q; intros; split; trivial|]. assert (H_bx:=Bounded_T_M_l _ _ _ _ _ _ _ _ H_bounded x Hx). assert (H_b1:=Bounded_T_M_3 _ _ _ _ _ _ _ _ H_bounded). assert (H_b2:=Bounded_T_M_4 _ _ _ _ _ _ _ _ H_bounded). assert (H_dx1:e*x+g+(f*x+h)<>Zero); [generalize (Bounded_M_nonzero_denum _ _ _ _ x H_b1 Hx_lr); rationalify_R_goal; intros H_tmp; assert (H_:=Q_to_R_Qneq _ _ H_tmp); ring_exact_Q H_|]. assert (H_dx2:f*x+h-(e*x+g)<>Zero); [generalize (Bounded_M_nonzero_denum _ _ _ _ x H_b2 Hx_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 * x + g + (f * x + h)))) (Qabs (Qone / (f * x + h - (e * x + g))))); [ stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e * x + g, f * x + h)) y1)); trivial; apply (maximum_eta_discriminant_base_interval _ _ _ _ y1 H_bx (proj1 Hy1) (proj2 Hy1)) | | stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e * x + g, f * x + h)) y2)); trivial; apply (maximum_eta_discriminant_base_interval _ _ _ _ y2 H_bx (proj1 Hy2) (proj2 Hy2)) | ]. apply Qmax_lub. apply Qle_trans with (Qmax (Qabs (Qone / (e + f + (g + h)))) (Qabs (Qone / (g + h - (e + f))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e + f, g + h)) x)). apply (maximum_eta_discriminant_base_interval (a+b) (c+d) (e+f) (g+h) x H_b1 (proj1 Hx) (proj2 Hx)). 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_2|apply (f_equal Qabs); field; ring_exact_Q H2]. apply Qle_trans with (Qmax (Qabs (Qone / (- e + f + (- g + h)))) (Qabs (Qone / (- g + h - (- e + f))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (-e + f, -g + h)) x)). apply (maximum_eta_discriminant_base_interval (-a+b) (-c+d) (-e+f) (-g+h) x H_b2 (proj1 Hx) (proj2 Hx)). 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_3|apply (f_equal Qabs); field; ring_exact_Q H3]. 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 + f + (g + h)))) (Qabs (Qone / (g + h - (e + f))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (e + f, g + h)) x)). apply (maximum_eta_discriminant_base_interval (a+b) (c+d) (e+f) (g+h) x H_b1 (proj1 Hx) (proj2 Hx)). 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_2|apply (f_equal Qabs); field; ring_exact_Q H2]. apply Qle_trans with (Qmax (Qabs (Qone / (- e + f + (- g + h)))) (Qabs (Qone / (- g + h - (- e + f))))). stepl (Qabs (as_Moebius_Q (0 / 1, 1 / 1, (-e + f, -g + h)) x)). apply (maximum_eta_discriminant_base_interval (-a+b) (-c+d) (-e+f) (-g+h) x H_b2 (proj1 Hx) (proj2 Hx)). 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_3|apply (f_equal Qabs); field; ring_exact_Q H3]. 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