proposition: Lemma maximum_eta_discriminant_base_interval: forall a b c d x, Bounded_M ((a,b),(c,d)) -> -Qone<= x -> x <=Qone -> Qabs (as_Moebius_Q ((0/1,1/1),(c,d)) x) <= Qmax (Qabs(Qone/(c+d))) (Qabs (Qone/(d-c))).
proof: Proof. intros a b c d x H_bounded Hx_l Hx_r. assert (Hdc_min:=Bounded_M_d_minus_c_nonzero _ _ _ _ H_bounded). assert (Hdc:=Bounded_M_c_plus_d_nonzero _ _ _ _ H_bounded). assert (Hx_lr:(-1<= x <= 1 )%R); [realify_Q; intros; split; trivial|]. generalize ((Bounded_M_denom_nonvanishing_M _ H_bounded) x Hx_lr). unfold denom_nonvanishing_M, fst, snd; rationalify_R_goal; intros Hcxd. destruct (Qle_dec_weak c Zero) as [Hc|Hc]. destruct (Q_le_lt_dec Zero (as_Moebius_Q (0 / 1, 1 / 1, (c, d)) x)) as [H_eta|H_eta]. rewrite (Qabs_eq _ H_eta). apply Qle_trans with (Qabs (Qone / (c + d))). apply Qle_trans with (Qone/(c+d)). apply maximum_eta_discriminant_nondecreasing with a b; trivial. apply Qle_Qabs. apply Qle_max_l. rewrite (Qabs_non_eq_neg _ H_eta). apply Qle_trans with (Qabs (Qone / (d-c))). apply Qle_trans with (Qopp (Qone/(d-c))). apply Qopp_Qle; apply minimum_eta_discriminant_nondecreasing with a b; trivial. apply Qle_Qabs_Qopp. apply Qle_max_r. destruct (Q_le_lt_dec Zero (as_Moebius_Q (0 / 1, 1 / 1, (c, d)) x)) as [H_eta|H_eta]. rewrite (Qabs_eq _ H_eta). apply Qle_trans with (Qabs (Qone / (d-c))). apply Qle_trans with (Qone/(d-c)). apply maximum_eta_discriminant_nonincreasing with a b; trivial. apply Qle_Qabs. apply Qle_max_r. rewrite (Qabs_non_eq_neg _ H_eta). apply Qle_trans with (Qabs (Qone / (c + d))). apply Qle_trans with (Qopp(Qone/(c+d))). apply Qopp_Qle; apply minimum_eta_discriminant_nonincreasing with a b; trivial. apply Qle_Qabs_Qopp. apply Qle_max_l. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs