proposition: Lemma Is_refining_M_property:forall mu r, ((-1)<=r<=1)%R->Is_refining_M mu -> ((-1)<=as_Moebius mu r<=1)%R.
proof: Proof. intros ((a,b),(c,d)) r Hr H_refining; generalize (Is_refining_M_denom_nonvanishing_M _ _ H_refining Hr). unfold denom_nonvanishing_M, as_Moebius, fst, snd. destruct (Is_refining_M_d_minusplus_c_sign_dec _ _ _ _ H_refining) as [[H1 [H2 [H3 [H4 [H7 [H5 H6]]]]]]|[H1 [H2 [H3 [H4 [H7 [H5 H6]]]]]]]; [ generalize (Is_refining_M_auxiliary_1 _ _ _ _ H1 H2 H3 H4) | generalize (Is_refining_M_auxiliary_2 _ _ _ _ H1 H2 H3 H4) ]; intros [H12 [H13 [H14 [H8 [H9 [H10 H11]]]]]]; realify_Q; intros H1 H2 H3 H4 H7 H5 H6 H12 H13 H14 H8 H9 H10 H11 H_denom. assert (H_crd:0<c*r+d); [ destruct (Qtrichotomy_inf Zero c) as [[Hc|Hc]|Hc]; realify_Q; intros Hc; [ apply Bounded_M_pos_auxiliary_1; trivial | rewrite <- Hc; stepr d; auto; ring | apply Bounded_M_pos_auxiliary_2; trivial] |]. split. destruct (Qtrichotomy_inf Zero (Qplus c a)) as [[Hca|Hca]|Hca]; realify_Q; intros Hca; (stepl (-1/1); [|field; auto]); apply Rmult_Rdiv_pos_Rle; auto; apply Rle_zero_Rminus; (stepr ((c+a)*r+(d+b)); [|ring]). apply Bounded_M_pos_auxiliary_3; trivial; ring_exact_R H4. rewrite <- Hca; stepr (d+b); auto; ring. apply Bounded_M_pos_auxiliary_4; trivial; ring_exact_R H1... destruct (Qtrichotomy_inf Zero (Qminus c a)) as [[Hca|Hca]|Hca]; realify_Q; intros Hca; (stepr (1/1); [|field; auto]); apply Rmult_Rdiv_pos_Rle; auto; apply Rle_zero_Rminus; (stepr ((c-a)*r+(d-b)); [|ring]). apply Bounded_M_pos_auxiliary_3; trivial; ring_exact_R H2. rewrite <- Hca; stepr (d-b); auto; ring. apply Bounded_M_pos_auxiliary_4; trivial; ring_exact_R H3... assert (H_crd:c*r+d<0); [ destruct (Qtrichotomy_inf Zero c) as [[Hc|Hc]|Hc]; realify_Q; intros Hc; [ apply Bounded_M_neg_auxiliary_1; trivial | rewrite <- Hc; stepl d; auto; ring | apply Bounded_M_neg_auxiliary_2; trivial] |]. split. destruct (Qtrichotomy_inf Zero (Qplus c a)) as [[Hca|Hca]|Hca]; realify_Q; intros Hca; (stepl (1/(-1)); [|field; auto]); apply Rmult_Rdiv_neg_Rle; auto; apply Rminus_le; (stepl ((c+a)*r+(d+b)); [|ring]). apply Bounded_M_neg_auxiliary_3; trivial; ring_exact_R H1. rewrite <- Hca; stepl (d+b); auto; ring. apply Bounded_M_neg_auxiliary_4; trivial; ring_exact_R H4... destruct (Qtrichotomy_inf Zero (Qminus c a)) as [[Hca|Hca]|Hca]; realify_Q; intros Hca; (stepr (-1/-1); [|field; auto]); apply Rmult_Rdiv_neg_Rle; auto; apply Rminus_le; (stepl ((c-a)*r+(d-b)); [|ring]). apply Bounded_M_neg_auxiliary_3; trivial; ring_exact_R H3. rewrite <- Hca; stepl (d-b); auto; ring. apply Bounded_M_neg_auxiliary_4; trivial; ring_exact_R H2... Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M