proposition: Lemma thesis_5_6_19:forall (eps:Q) xi H_xi, Zero < eps -> { theta1:Q & {theta2 | Zero<theta1/\Zero<theta2/\ (forall x1 y1 x2 y2 (Hx1:-Qone<=x1/\x1<=Qone) (Hy1:-Qone<=y1/\y1<=Qone) (Hx2:-Qone<=x2/\x2<=Qone) (Hy2:-Qone<=y2/\y2<=Qone), Qabs (x1-x2)<theta1 -> Qabs (y1-y2)<theta2 ->diameter2 xi H_xi x1 y1 x2 y2 Hx1 Hy1 Hx2 Hy2 < eps) }}.
proof: Proof. intros eps xi H_xi H_eps. destruct (upper_bound_diameter2 eps xi H_xi H_eps) as [theta1 [theta2 [H_theta1 [H_theta2 H_theta]]]]. exists theta1; exists theta2; repeat split; trivial. intros x1 y1 x2 y2 Hx1 Hy1 Hx2 Hy2 H_x1y1 H_x2y2. unfold diameter2. assert (H_x1x1:Qabs (x1 - x1) < theta1); [stepl (Qabs Zero); trivial; apply (f_equal Qabs); ring|]. assert (H_y1y1:Qabs (y1 - y1) < theta2); [stepl (Qabs Zero); trivial; apply (f_equal Qabs); ring|]. assert (H_x2x2:Qabs (x2 - x2) < theta1); [stepl (Qabs Zero); trivial; apply (f_equal Qabs); ring|]. assert (H_y2y2:Qabs (y2 - y2) < theta2); [stepl (Qabs Zero); trivial; apply (f_equal Qabs); ring|]. assert (H_x2x1:Qabs (x2 - x1) < theta1); [rewrite Qabs_Qminus_sym; trivial|]. assert (H_y2y1:Qabs (y2 - y1) < theta2); [rewrite Qabs_Qminus_sym; trivial|]. set (xi_ll:= as_Tensor_Q xi x1 y1); set (xi_lr:= as_Tensor_Q xi x1 y2); set (xi_rl:= as_Tensor_Q xi x2 y1); set (xi_rr:= as_Tensor_Q xi x2 y2). destruct (Qmax4_informative xi_ll xi_lr xi_rl xi_rr) as [[[Hmax|Hmax]|Hmax]|Hmax]; destruct (Qmin4_informative xi_ll xi_lr xi_rl xi_rr) as [[[Hmin|Hmin]|Hmin]|Hmin]; rewrite Hmax; rewrite Hmin; unfold xi_ll, xi_lr, xi_rl, xi_rr; match goal with | |- as_Tensor_Q xi ?X1 ?Y1 - as_Tensor_Q xi ?X2 ?Y2 < eps => apply Qle_lt_trans with (Qabs (as_Tensor_Q xi X1 Y1 - as_Tensor_Q xi X2 Y2)); [apply Qle_Qabs| apply (H_theta X1 Y1 X2 Y2)]; trivial end. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M