proposition: Lemma denom_nonvanishing_T_within_diameter2: 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 -> let xi_ll:= as_Tensor_Q xi (-Qone) (-Qone) in let xi_lr:= as_Tensor_Q xi (-Qone) Qone in let xi_rl:= as_Tensor_Q xi Qone (-Qone) in let xi_rr:= as_Tensor_Q xi Qone Qone in (Qmin4 xi_ll xi_lr xi_rl xi_rr <= as_Tensor xi r1 r2 <= Qmax4 xi_ll xi_lr xi_rl xi_rr)%R.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_denom r1 r2 Hr1 Hr2 xi_ll xi_lr xi_rl xi_rr. assert (H_bounded:=(denom_nonvanishing_T_Bounded_T _ H_denom)). 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_bounded1:=Bounded_T_M_1 _ _ _ _ _ _ _ _ H_bounded); assert (H_bounded2:=Bounded_T_M_2 _ _ _ _ _ _ _ _ H_bounded). generalize (H_denom _ _ Hr1 Hr2). unfold denom_nonvanishing_T, as_Tensor, fst, snd. intros H_efgh. destruct (Rle_dec_weak 0 ((a*r2+b)*(g*r2+h)-(c*r2+d)*(e*r2+f))) as [H_det2|H_det2]; split. apply Rle_trans with (((Qminus c a)*r2+(Qminus d b))/((Qminus g e)*r2+(Qminus h f)))%R. destruct (Qle_dec_weak 0 ((c-a)*(h-f)-(d-b)*(g-e))) as [H_det|H_det]. apply Rle_trans with (((a-c)+(d-b))/((e-g)+(h-f)))%R. rationalify_R; trivial; stepr xi_ll; [apply Qle_Qmin4_1|subst xi_ll; unfold as_Tensor_Q, fst,snd; field; trivial]. stepl (((Qminus c a)*(-1)+(Qminus d b))/((Qminus g e)*(-1)+(Qminus h f)))%R. apply (det_nonneg_nondecreasing (c-a) (d-b) (g-e) (h-f) (-1)%R r2 H_bounded1 H_det min_one_is_in_base_interval Hr2 (proj1 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((c-a)+(d-b))/((g-e)+(h-f)))%R. rationalify_R; trivial; stepr xi_lr; [apply Qle_Qmin4_2|subst xi_lr; unfold as_Tensor_Q, fst,snd; field; trivial]. stepl (((Qminus c a)*1+(Qminus d b))/((Qminus g e)*1+(Qminus h f)))%R. apply (det_nonpos_nonincreasing (c-a) (d-b) (g-e) (h-f) r2 (1)%R H_bounded1 H_det Hr2 one_is_in_base_interval (proj2 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... stepl ((a*(-1)*r2+b*(-1)+c*r2+d)/(e*(-1)*r2+f*(-1)+g*r2+h))%R. apply (det2_nonneg_nondecreasing _ _ _ _ _ _ _ _ _ _ _ H_bounded Hr2 H_det2 min_one_is_in_base_interval Hr1 (proj1 Hr1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((Qplus a c)*r2+(Qplus b d))/((Qplus e g)*r2+(Qplus f h)))%R. stepr ((a*1*r2+b*1+c*r2+d)/(e*1*r2+f*1+g*r2+h))%R. apply (det2_nonneg_nondecreasing _ _ _ _ _ _ _ _ _ _ _ H_bounded Hr2 H_det2 Hr1 one_is_in_base_interval (proj2 Hr1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... destruct (Qle_dec_weak 0 ((a+c)*(f+h)-(b+d)*(e+g))) as [H_det|H_det]. apply Rle_trans with (((a+c)+(b+d))/((e+g)+(f+h)))%R. stepr (((Qplus a c)*1+(Qplus b d))/((Qplus e g)*(1)+(Qplus f h)))%R. apply (det_nonneg_nondecreasing (a+c) (b+d) (e+g) (f+h) r2 (1)%R H_bounded2 H_det Hr2 one_is_in_base_interval (proj2 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; trivial; stepl xi_rr; [apply Qle_Qmax4_4|subst xi_rr; unfold as_Tensor_Q, fst,snd; field; trivial]. apply Rle_trans with (((b+d)-(a+c))/((f+h)-(e+g)))%R. stepr (((Qplus a c)*(-1)+(Qplus b d))/((Qplus e g)*(-1)+(Qplus f h)))%R. apply (det_nonpos_nonincreasing (a+c) (b+d) (e+g) (f+h) (-1)%R r2 H_bounded2 H_det min_one_is_in_base_interval Hr2 (proj1 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; trivial; stepl xi_rl; [apply Qle_Qmax4_3|subst xi_rl; unfold as_Tensor_Q, fst,snd; field; trivial]. apply Rle_trans with (((Qplus a c)*r2+(Qplus b d))/((Qplus e g)*r2+(Qplus f h)))%R. destruct (Qle_dec_weak 0 ((a+c)*(f+h)-(b+d)*(e+g))) as [H_det|H_det]. apply Rle_trans with (((b+d)-(a+c))/((f+h)-(e+g)))%R. rationalify_R; trivial; stepr xi_rl; [apply Qle_Qmin4_3|subst xi_rl; unfold as_Tensor_Q, fst,snd; field; trivial]. stepl (((Qplus a c)*(-1)+(Qplus b d))/((Qplus e g)*(-1)+(Qplus f h)))%R. apply (det_nonneg_nondecreasing (a+c) (b+d) (e+g) (f+h) (-1)%R r2 H_bounded2 H_det min_one_is_in_base_interval Hr2 (proj1 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((a+c)+(b+d))/((e+g)+(f+h)))%R. rationalify_R; trivial; stepr xi_rr; [apply Qle_Qmin4_4|subst xi_rr; unfold as_Tensor_Q, fst,snd; field; trivial]. stepl (((Qplus a c)*1+(Qplus b d))/((Qplus e g)*(1)+(Qplus f h)))%R. apply (det_nonpos_nonincreasing (a+c) (b+d) (e+g) (f+h) r2 (1)%R H_bounded2 H_det Hr2 one_is_in_base_interval (proj2 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... stepl ((a*1*r2+b*1+c*r2+d)/(e*1*r2+f*1+g*r2+h))%R. apply (det2_nonpos_nonincreasing _ _ _ _ _ _ _ _ _ _ _ H_bounded Hr2 H_det2 Hr1 one_is_in_base_interval (proj2 Hr1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((Qminus c a)*r2+(Qminus d b))/((Qminus g e)*r2+(Qminus h f)))%R. stepr ((a*(-1)*r2+b*(-1)+c*r2+d)/(e*(-1)*r2+f*(-1)+g*r2+h))%R. apply (det2_nonpos_nonincreasing _ _ _ _ _ _ _ _ _ _ _ H_bounded Hr2 H_det2 min_one_is_in_base_interval Hr1 (proj1 Hr1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... destruct (Qle_dec_weak 0 ((c-a)*(h-f)-(d-b)*(g-e))) as [H_det|H_det]. apply Rle_trans with (((c-a)+(d-b))/((g-e)+(h-f)))%R. stepr (((Qminus c a)*1+(Qminus d b))/((Qminus g e)*1+(Qminus h f)))%R. apply (det_nonneg_nondecreasing (c-a) (d-b) (g-e) (h-f) r2 (1)%R H_bounded1 H_det Hr2 one_is_in_base_interval (proj2 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; trivial; stepl xi_lr; [apply Qle_Qmax4_2|subst xi_lr; unfold as_Tensor_Q, fst,snd; field; trivial]. apply Rle_trans with (((a-c)+(d-b))/((e-g)+(h-f)))%R. stepr (((Qminus c a)*(-1)+(Qminus d b))/((Qminus g e)*(-1)+(Qminus h f)))%R. apply (det_nonpos_nonincreasing (c-a) (d-b) (g-e) (h-f) (-1)%R r2 H_bounded1 H_det min_one_is_in_base_interval Hr2 (proj1 Hr2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; trivial; stepl xi_ll; [apply Qle_Qmax4_1|subst xi_ll; unfold as_Tensor_Q, fst,snd; field; trivial]. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs