proposition: Lemma upper_bound_diameter2:forall (eps:Q) xi (H_xi:Is_refining_T xi) (H_eps: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 -> Qabs ((as_Tensor_Q xi x1 y1)-(as_Tensor_Q xi x2 y2)) < eps)}}.
proof: Proof. intros eps xi H_xi H_eps. destruct (upper_bound_Tensor_Moebius_Q_l _ H_xi) as [Kl [HKl_1 HKl_2]]. destruct (upper_bound_Tensor_Moebius_Q_r _ H_xi) as [Kr [HKr_1 HKr_2]]. exists (eps/(2*Kr)); exists (eps/(2*Kl)); repeat split; [ qZ_numerals; unfold Qdiv; auto | qZ_numerals; unfold Qdiv; auto | ]. intros x1 y1 x2 y2 Hx1 Hy1 Hx2 Hy2 Hx1x2 Hy1y2. stepl (Qabs ((as_Tensor_Q xi x1 y1 - as_Tensor_Q xi x2 y1)+(as_Tensor_Q xi x2 y1 - as_Tensor_Q xi x2 y2))); [|apply (f_equal Qabs); ring]. apply Qle_lt_trans with ((Qabs (as_Tensor_Q xi x1 y1 - as_Tensor_Q xi x2 y1)) +(Qabs (as_Tensor_Q xi x2 y1 - as_Tensor_Q xi x2 y2))); [apply Qabs_triangle|]. stepr ((eps/2)*Qone+(eps/2)*Qone); [|qZ_numerals; field; auto]. destruct (Qle_lt_eq_dec _ _ (Qabs_nonneg (x1-x2))) as [Habsx|Habsx]; destruct (Qle_lt_eq_dec _ _ (Qabs_nonneg (y1-y2))) as [Habsy|Habsy]. apply Qlt_plus_plus; [ apply Qlt_transitive with (Kr * Qabs (x1 - x2)); [apply (HKr_2 x1 x2 y1); assumption|] | apply Qlt_transitive with (Kl * Qabs (y1 - y2)); [apply (HKl_2 x2 y1 y2); assumption|] ]; rewrite Qmult_sym; apply Qdiv_Qmult_pos; auto; rewrite Qdiv_Qdiv_Qmult_numerator; auto; [ stepl (Qabs (x1 - x2)) | stepl (Qabs (y1 - y2))]; trivial; field; auto... apply Qlt_plus_plus; [ apply Qlt_transitive with (Kr * Qabs (x1 - x2)); [apply (HKr_2 x1 x2 y1); assumption|]; rewrite Qmult_sym; apply Qdiv_Qmult_pos; auto; rewrite Qdiv_Qdiv_Qmult_numerator; auto; stepl (Qabs (x1 - x2)); trivial; field; auto | stepl Zero; [ qZ_numerals; unfold Qdiv; auto | rewrite (Qabs_Qminus_Zero_eq _ _ (sym_eq Habsy)); symmetry; apply Qabs_Zero_Qminus_eq; reflexivity ] ]... apply Qlt_plus_plus; [ stepl Zero; [ qZ_numerals; unfold Qdiv; auto | rewrite (Qabs_Qminus_Zero_eq _ _ (sym_eq Habsx)); symmetry; apply Qabs_Zero_Qminus_eq; reflexivity ] | apply Qlt_transitive with (Kl * Qabs (y1 - y2)); [apply (HKl_2 x2 y1 y2); assumption|]; rewrite Qmult_sym; apply Qdiv_Qmult_pos; auto; rewrite Qdiv_Qdiv_Qmult_numerator; auto; stepl (Qabs (y1 - y2)); trivial; field; auto ]... apply Qlt_plus_plus; [ stepl Zero; [ qZ_numerals; unfold Qdiv; auto | rewrite (Qabs_Qminus_Zero_eq _ _ (sym_eq Habsx)); symmetry; apply Qabs_Zero_Qminus_eq; reflexivity ] | stepl Zero; [ qZ_numerals; unfold Qdiv; auto | rewrite (Qabs_Qminus_Zero_eq _ _ (sym_eq Habsy)); symmetry; apply Qabs_Zero_Qminus_eq; reflexivity ] ]... Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M