proposition: Lemma Incl_T_R_folded: forall xi, (forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> denom_nonvanishing_T xi r1 r2) -> (forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> (0 <= as_Tensor xi r1 r2 <= 1)%R) -> Incl_T xi RR.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_denom H_xi. assert (H_bounded:=(denom_nonvanishing_T_Bounded_T _ H_denom)). unfold as_Tensor in H_xi; simpl in H_xi. assert (H_efgh1:=Bounded_T_e_mf_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh2:=Bounded_T_me_mf_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh3:=Bounded_T_me_f_mg_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_efgh4:=Bounded_T_e_f_g_h_nonzero _ _ _ _ _ _ _ _ H_bounded); assert (H_h:=Bounded_T_nonzero _ _ _ _ _ _ _ _ H_bounded). unfold Incl_T, map_digits, fst, snd; qZ_numerals; repeat split; trivial. destruct (not_Qeq_inf _ _ H_efgh1) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh1m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + - b + - c + d)%R); apply Rdiv_Rmult_pos_neg_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(-1)*(-1)+b*(-1)+c*(-1)+d)/(e*(-1)*(-1)+f*(-1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh1]; exact (proj1 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + - b + - c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(-1)*(-1)+b*(-1)+c*(-1)+d)/(e*(-1)*(-1)+f*(-1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh1]; exact (proj1 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh1) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh1m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + - b + - c + d)%R); apply Rdiv_Rmult_neg_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(-1)*(-1)+b*(-1)+c*(-1)+d)/(e*(-1)*(-1)+f*(-1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh1]; exact (proj2 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + - b + - c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(-1)*(-1)+b*(-1)+c*(-1)+d)/(e*(-1)*(-1)+f*(-1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh1]; exact (proj2 (H_xi (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh2) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh2m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + - b + c + d)%R); apply Rdiv_Rmult_pos_neg_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(-1)*(1)+b*(-1)+c*(1)+d)/(e*(-1)*(1)+f*(-1)+g*(1)+h))%R; [|field; ring_exact_R H_efgh2]; exact (proj1 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + - b + c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(-1)*(1)+b*(-1)+c*(1)+d)/(e*(-1)*(1)+f*(-1)+g*(1)+h))%R; [|field; ring_exact_R H_efgh2]; exact (proj1 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh2) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh2m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + - b + c + d)%R); apply Rdiv_Rmult_neg_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(-1)*(1)+b*(-1)+c*(1)+d)/(e*(-1)*(1)+f*(-1)+g*(1)+h))%R; [|field; ring_exact_R H_efgh2]; exact (proj2 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + - b + c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(-1)*(1)+b*(-1)+c*(1)+d)/(e*(-1)*(1)+f*(-1)+g*(1)+h))%R; [|field; ring_exact_R H_efgh2]; exact (proj2 (H_xi (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh3) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh3m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + b + -c + d)%R); apply Rdiv_Rmult_pos_neg_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(1)*(-1)+b*(1)+c*(-1)+d)/(e*(1)*(-1)+f*(1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh3]; exact (proj1 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + b + -c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*(1)*(-1)+b*(1)+c*(-1)+d)/(e*(1)*(-1)+f*(1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh3]; exact (proj1 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh3) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh3m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + b + -c + d)%R); apply Rdiv_Rmult_neg_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(1)*(-1)+b*(1)+c*(-1)+d)/(e*(1)*(-1)+f*(1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh3]; exact (proj2 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (-a + b + -c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*(1)*(-1)+b*(1)+c*(-1)+d)/(e*(1)*(-1)+f*(1)+g*(-1)+h))%R; [|field; ring_exact_R H_efgh3]; exact (proj2 (H_xi (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh4) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh4m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + b + c + d)%R); apply Rdiv_Rmult_pos_neg_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*1*1+b*1+c*1+d)/(e*1*1+f*1+g*1+h))%R; [|field; ring_exact_R H_efgh4]; exact (proj1 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + b + c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepl R0; [|field]; stepr ((a*1*1+b*1+c*1+d)/(e*1*1+f*1+g*1+h))%R; [|field; ring_exact_R H_efgh4]; exact (proj1 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval)). destruct (not_Qeq_inf _ _ H_efgh4) as [H_|H_]; apply Q_to_R_Qle; realify_Q; auto; intros H_efgh1 H_efgh2 H_efgh3 H_efgh4 H_h H_egh4m. apply Rmult_le_compat_neg_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + b + c + d)%R); apply Rdiv_Rmult_neg_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*1*1+b*1+c*1+d)/(e*1*1+f*1+g*1+h))%R; [|field; ring_exact_R H_efgh4]; exact (proj2 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval)). apply Rmult_le_compat_l; [Fourier.fourier|]; rewrite (Rmult_comm (a + b + c + d)%R); apply Rdiv_Rmult_pos_pos_Rle'; auto; try Fourier.fourier; stepr R1; [|field]; stepl ((a*1*1+b*1+c*1+d)/(e*1*1+f*1+g*1+h))%R; [|field; ring_exact_R H_efgh4]; exact (proj2 (H_xi (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval)). Qed.
imports: digits Bounded_M Bounded_T Incl_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs