proposition: Lemma Is_refining_M_property_fold: forall mu, (forall r, (-1 <= r <= 1)%R -> denom_nonvanishing_M mu r)-> (forall (r : R),(-1 <= r <= 1)%R -> (-1<=as_Moebius mu r<=1)%R) -> Is_refining_M mu.
proof: Proof. intros ((a,b),(c,d)) H_denom H_mu. unfold denom_nonvanishing_M in H_denom; simpl in H_denom. unfold as_Moebius in H_mu; simpl in H_mu. assert (H_dcmin:d-c <>Zero); [apply Q_to_R_Qneq; realify_Q; stepl (c*(-1)+d)%R; [|ring]; apply (H_denom (-1)%R min_one_is_in_base_interval)|]. assert (H_dc:d+c <>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (c*1+d)%R; [|ring]; apply (H_denom (1)%R one_is_in_base_interval)|]. assert (Hd: d<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (c*0+d)%R; [|ring]; apply H_denom; split; fourier|]. split; [ apply denom_nonvanishing_M_Bounded_M; assumption|]. simpl. destruct (denom_nonvanishing_M_Bounded_M ((a,b),(c,d)) H_denom) as [[H1 H2]|[H1 H2]]; simpl in H1, H2. left; repeat split. apply Qle_Qdiv_denom_pos_nonneg with (d+c); trivial; assert (Hcd:c*Qone+d <> Zero);[stepl (d+c); trivial; ring|]; stepr (((a*Qone + b)/(c*Qone + d)) - (- Qone)); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj1 (H_mu (1)%R one_is_in_base_interval)). apply Qle_Qdiv_denom_pos_nonneg with (d-c); trivial; assert (Hcd:c*(-Qone)+d <> Zero);[stepl (d-c); trivial; ring|]; stepr (Qone -((a*(-Qone) + b)/(c*(-Qone) + d))); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj2 (H_mu (-1)%R min_one_is_in_base_interval)). apply Qle_Qdiv_denom_pos_nonneg with (d+c); trivial; assert (Hcd:c*Qone+d <> Zero);[stepl (d+c); trivial; ring|]; stepr (Qone-((a*Qone + b)/(c*Qone + d))); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj2 (H_mu (1)%R one_is_in_base_interval)). apply Qle_Qdiv_denom_pos_nonneg with (d-c); trivial; assert (Hcd:c*(-Qone)+d <> Zero);[stepl (d-c); trivial; ring|]; stepr (((a*(-Qone) + b)/(c*(-Qone) + d))-(-Qone)); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj1 (H_mu (-1)%R min_one_is_in_base_interval)). right; repeat split. apply Qle_Qdiv_denom_neg_nonneg with (d+c); trivial; assert (Hcd:c*Qone+d <> Zero);[stepl (d+c); trivial; ring|]; stepr (((a*Qone + b)/(c*Qone + d)) - (- Qone)); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj1 (H_mu (1)%R one_is_in_base_interval)). apply Qle_Qdiv_denom_neg_nonneg with (d-c); trivial; assert (Hcd:c*(-Qone)+d <> Zero);[stepl (d-c); trivial; ring|]; stepr (Qone -((a*(-Qone) + b)/(c*(-Qone) + d))); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj2 (H_mu (-1)%R min_one_is_in_base_interval)). apply Qle_Qdiv_denom_neg_nonneg with (d+c); trivial; assert (Hcd:c*Qone+d <> Zero);[stepl (d+c); trivial; ring|]; stepr (Qone-((a*Qone + b)/(c*Qone + d))); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj2 (H_mu (1)%R one_is_in_base_interval)). apply Qle_Qdiv_denom_neg_nonneg with (d-c); trivial; assert (Hcd:c*(-Qone)+d <> Zero);[stepl (d-c); trivial; ring|]; stepr (((a*(-Qone) + b)/(c*(-Qone) + d))-(-Qone)); [|field; auto]; apply Qle_Qminus_Zero; apply Q_to_R_Qle; realify_Q_goal; trivial; apply (proj1 (H_mu (-1)%R min_one_is_in_base_interval)). Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M