proposition: Lemma rasterize1_close : l < r -> forall (n:positive) (x:Q), Qabs (x - f n (rasterize1 n x)) <= ((r-l)/((2#1) * inject_Z (Zpos n))).
proof: Proof. clear Hlr. intros Hlr' n x. rewrite -> Qlt_minus_iff in Hlr'. assert (A:~ r - l == 0 /\ ~ inject_Z (Zpos n) == 0) by (split;auto with *;discriminate). setoid_replace ((r - l) / ((2#1) * inject_Z (Zpos n))) with ((1#2)/(inject_Z (Zpos n)/(r - l))) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field; auto). apply Qle_shift_div_l. apply Qlt_shift_div_l; auto with *. rewrite <- (Qabs_pos (inject_Z (Zpos n)/(r-l))); [|apply Qle_shift_div_l; auto with *]. rewrite <- Qabs_Qmult. unfold f. change (2*Zpos n # 1) with ((2#1)*inject_Z (Zpos n)). setoid_replace ((x - (l + (r - l) * (2 * rasterize1 n x + 1 # 1) / ((2#1) * inject_Z (Zpos n)))) * (inject_Z (Zpos n) / (r - l))) with (inject_Z (Zpos n)*(x-l)/(r-l) - (2*rasterize1 n x + 1 # 1)/(2#1)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field; auto). rewrite -> Qmake_Qdiv. rewrite Q.Zplus_Qplus. unfold Qdiv. change (inject_Z 1) with 1%Q. rewrite Qmult_1_r. rewrite Q.Zmult_Qmult. change (inject_Z 2) with (2#1). setoid_replace (((2#1) * inject_Z (rasterize1 n x) + 1) / (2#1)) with (inject_Z (rasterize1 n x) + (1#2)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field; auto). unfold rasterize1. unfold Qdiv. generalize (inject_Z (Zpos n) * (x - l) * / (r - l)). intros q. clear - q. apply Qabs_case; intros H; rewrite -> Qle_minus_iff. setoid_replace ((1 # 2) + - (q - (inject_Z (Qfloor q) + (1 # 2)))) with (inject_Z (Qfloor q) + 1 + - q) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. apply Qlt_le_weak. change 1 with (inject_Z 1). rewrite <- (Q.Zplus_Qplus (Qfloor q) 1). apply Qlt_floor. setoid_replace ((1 # 2) + - - (q - (inject_Z (Qfloor q) + (1 # 2)))) with (q + -inject_Z (Qfloor q)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. apply Qfloor_le. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact CoRN.metric2.LocatedSubset CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.metric2.Qmetric Coq.QArith.Qround Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Classic