proposition: Lemma thesis_5_6_20:forall xi H_refining, diameter2 xi H_refining (-Qone) (-Qone) Qone Qone min_one_is_in_base_interval_Q min_one_is_in_base_interval_Q one_is_in_base_interval_Q one_is_in_base_interval_Q < redundancy -> {d:Digit| Incl_T xi d}.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_refining. assert (H_bounded:=proj1 H_refining). assert (H_denom:forall r1 r2,(-1<=r1<=1)%R->(-1<=r2<=1)%R->denom_nonvanishing_T (a,b,(c,d),(e,f,(g,h))) r1 r2); [intros r1 r2 Hr1 Hr2; apply Is_refining_T_denom_nonvanishing_T; trivial|]. unfold diameter2,redundancy. set (xi_ll:= as_Tensor_Q (((a,b),(c,d)),((e,f),(g,h))) (-Qone) (-Qone)); set (xi_lr:= as_Tensor_Q (((a,b),(c,d)),((e,f),(g,h))) (-Qone) Qone); set (xi_rl:= as_Tensor_Q (((a,b),(c,d)),((e,f),(g,h))) Qone (-Qone)); set (xi_rr:= as_Tensor_Q (((a,b),(c,d)),((e,f),(g,h))) Qone Qone). set (M:=Qmax4 xi_ll xi_lr xi_rl xi_rr). set (m:=Qmin4 xi_ll xi_lr xi_rl xi_rr). intros H_diam. destruct (Q_le_lt_dec M Zero) as [H_M|H_M]. exists LL. apply Incl_T_L_folded; trivial; intros r1 r2 Hr1 Hr2; split. elim (Is_refining_T_property _ _ _ Hr1 Hr2 H_refining); trivial. apply Rle_trans with M; [ | realify_Q; auto]; exact (proj2 (denom_nonvanishing_T_within_diameter2 _ H_denom _ _ Hr1 Hr2)). destruct (Q_le_lt_dec Zero m) as [H_m|H_m]. exists RR. apply Incl_T_R_folded; trivial; intros r1 r2 Hr1 Hr2; split. apply Rle_trans with m; [ realify_Q; auto| ]; exact (proj1 (denom_nonvanishing_T_within_diameter2 _ H_denom _ _ Hr1 Hr2)). elim (Is_refining_T_property _ _ _ Hr1 Hr2 H_refining); trivial. exists MM. apply Incl_T_M_folded; trivial; intros r1 r2 Hr1 Hr2; split. apply Rle_trans with m. generalize (Q_to_Rlt _ _ H_M); assert (H_diam':(M-m<1/3)%R); [ generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_M'; fourier ]... exact (proj1 (denom_nonvanishing_T_within_diameter2 _ H_denom _ _ Hr1 Hr2))... apply Rle_trans with M. exact (proj2 (denom_nonvanishing_T_within_diameter2 _ H_denom _ _ Hr1 Hr2))... generalize (Q_to_Rlt _ _ H_m); assert (H_diam':(M-m<1/3)%R); [ generalize (Q_to_Rlt _ _ H_diam); rationalify_R_goal | realify_Q_goal; intros H_M'; fourier ]... Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M