proposition: Lemma thesis_5_6_9:forall mu H_refining, diameter mu H_refining < redundancy -> {d:Digit| Incl_M mu d}.
proof: Proof. intros ((a,b),(c,d)) H_refining. assert (H_bounded:=proj1 H_refining). assert (H_denom: forall r : R, (-1 <= r <= 1)%R -> denom_nonvanishing_M (a, b, (c, d)) r); [intros r Hr; apply Is_refining_M_denom_nonvanishing_M; trivial|]. set (mu_1:=as_Moebius_Q ((a,b),(c,d)) Qone). set (mu_2:=as_Moebius_Q ((a,b),(c,d)) (- Qone)). destruct (Qle_dec_weak (a*d-b*c) Zero) as [H_det|H_det]; unfold diameter,redundancy; fold mu_1 mu_2. assert (H_mu:=det_nonpos_refining_endpoints _ _ _ _ H_refining H_det); fold mu_1 mu_2 in H_mu. rewrite (Qabs_non_eq _ (Qle_Qminus_Zero_neg _ _ H_mu)); intro H_diam. destruct (Q_le_lt_dec mu_2 Zero) as [H_mu_2|H_mu_2]. exists LL. apply Incl_M_L_folded; trivial; intros r Hr; split. elim (Is_refining_M_property _ _ Hr H_refining); trivial. apply Rle_trans with mu_2; [ | realify_Q; auto]. generalize (det_nonpos_nonincreasing _ _ _ _ (-1) r H_bounded H_det min_one_is_in_base_interval Hr (proj1 Hr)); unfold mu_2, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d-c); try ring; t_local ]. destruct (Q_le_lt_dec Zero mu_1) as [H_mu_1|H_mu_1]. exists RR. apply Incl_M_R_folded; trivial; intros r Hr; split. apply Rle_trans with mu_1; [ realify_Q; auto| ]. generalize (det_nonpos_nonincreasing _ _ _ _ r 1 H_bounded H_det Hr one_is_in_base_interval (proj2 Hr)); unfold mu_1, as_Moebius_Q, as_Moebius; simpl. let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d+c); try ring; t_local ]. elim (Is_refining_M_property _ _ Hr H_refining); trivial. exists MM. apply Incl_M_M_folded; trivial; intros r Hr; split. apply Rle_trans with mu_1. generalize (Q_to_Rlt _ _ H_mu_2); assert (H_diam':(mu_2-mu_1<1/3)%R); [ stepl (-(mu_1 - mu_2))%R; [|ring]; generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_mu_2'; fourier ]... generalize (det_nonpos_nonincreasing _ _ _ _ r 1 H_bounded H_det Hr one_is_in_base_interval (proj2 Hr)); unfold mu_1, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d+c); try ring; t_local ]... apply Rle_trans with mu_2. generalize (det_nonpos_nonincreasing _ _ _ _ (-1) r H_bounded H_det min_one_is_in_base_interval Hr (proj1 Hr)); unfold mu_2, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d-c); try ring; t_local ]... generalize (Q_to_Rlt _ _ H_mu_1); assert (H_diam':(mu_2-mu_1<1/3)%R); [ stepl (-(mu_1 - mu_2))%R; [|ring]; generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_mu_2'; fourier ]... assert (H_mu:=det_nonneg_refining_endpoints _ _ _ _ H_refining H_det); fold mu_1 mu_2 in H_mu. rewrite (Qabs_eq _ (Qle_Qminus_Zero _ _ H_mu)); intro H_diam. destruct (Q_le_lt_dec mu_1 Zero) as [H_mu_1|H_mu_1]. exists LL. apply Incl_M_L_folded; trivial; intros r Hr; split. elim (Is_refining_M_property _ _ Hr H_refining); trivial. apply Rle_trans with mu_1; [ | realify_Q; auto]. generalize (det_nonneg_nondecreasing _ _ _ _ r 1 H_bounded H_det Hr one_is_in_base_interval (proj2 Hr)); unfold mu_1, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d+c); try ring; t_local ]. destruct (Q_le_lt_dec Zero mu_2) as [H_mu_2|H_mu_2]. exists RR. apply Incl_M_R_folded; trivial; intros r Hr; split. apply Rle_trans with mu_2; [ realify_Q; auto| ]. generalize (det_nonneg_nondecreasing _ _ _ _ (-1) r H_bounded H_det min_one_is_in_base_interval Hr (proj1 Hr)); unfold mu_2, as_Moebius_Q, as_Moebius; simpl. let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d-c); try ring; t_local ]. elim (Is_refining_M_property _ _ Hr H_refining); trivial. exists MM. apply Incl_M_M_folded; trivial; intros r Hr; split. apply Rle_trans with mu_2. generalize (Q_to_Rlt _ _ H_mu_1); assert (H_diam':(mu_1-mu_2<1/3)%R); [ generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_mu_2'; fourier ]... generalize (det_nonneg_nondecreasing _ _ _ _ (-1) r H_bounded H_det min_one_is_in_base_interval Hr (proj1 Hr)); unfold mu_2, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d-c); try ring; t_local ]... apply Rle_trans with mu_1. generalize (det_nonneg_nondecreasing _ _ _ _ r 1 H_bounded H_det Hr one_is_in_base_interval (proj2 Hr)); unfold mu_1, as_Moebius_Q, as_Moebius; simpl; let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in realify_Q_goal; [ trivial | stepl (d+c); try ring; t_local ]... generalize (Q_to_Rlt _ _ H_mu_2); assert (H_diam':(mu_1-mu_2<1/3)%R); [ generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_mu_2'; fourier ]... Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M