proposition: Lemma rasterize1_error : forall l (w:Qpos) n x, (l <= x <= l + proj1_sig w) -> Qball ((1 #2*n) * proj1_sig w) (C l (l + proj1_sig w) n (Z.min (Z.pos n -1) (Z.max 0 (rasterize1 l (l+proj1_sig w) n x)))) x.
proof: Proof. clear - C. intros l w n x H0. destruct (Qlt_le_dec x (l+proj1_sig w)). - replace (Z.min (Z.pos n -1) (Z.max 0 (rasterize1 l (l + proj1_sig w) n x))) with (rasterize1 l (l + proj1_sig w) n x). + apply ball_sym. simpl. rewrite -> Qball_Qabs. assert (l < l + proj1_sig w). { rewrite -> Qlt_minus_iff. ring_simplify. exact (Qpos_ispos w). } eapply Qle_trans. unfold C. apply (rasterize1_close H). setoid_replace (l + proj1_sig w - l) with (proj1_sig w) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). unfold Qdiv. rewrite Qmult_comm. apply Qmult_le_compat_r. apply Qle_refl. apply Qpos_nonneg. + rewrite Z.max_r. apply Z.min_case_strong. intros H. apply Zle_antisym; auto. apply Zlt_succ_le. rewrite <- Z.add_1_r. replace (Z.pos n - 1 + 1)%Z with (Z.pos n) by ring. apply rasterize1_boundR; auto. rewrite -> Qle_minus_iff. ring_simplify. exact (Qpos_nonneg w). reflexivity. destruct H0. apply rasterize1_boundL; auto. apply Qle_trans with x; auto. - rewrite Z.min_l. setoid_replace x with (l + proj1_sig w). apply ball_sym. rewrite -> Qball_Qabs. unfold C. rewrite <- (Qmult_comm (proj1_sig w)). change (1 # 2*n) with (/((2#1)*inject_Z (Z.pos n))). change (2*Z.pos n #1) with ((2#1)*inject_Z (Z.pos n)). replace (2 * (Z.pos n - 1) + 1)%Z with (2*Z.pos n + - 1)%Z by ring. change (2*Z.pos n + -1#1) with (inject_Z (2*Z.pos n + - 1)). rewrite -> Q.Zplus_Qplus. rewrite -> Q.Zmult_Qmult. change (inject_Z 2) with (2#1). change (inject_Z (-1)) with (-1#1)%Q. setoid_replace (l + proj1_sig w - (l + (l + proj1_sig w - l) * ((2#1) * inject_Z (Z.pos n) + (-1#1)) / ((2#1) * (inject_Z (Z.pos n))))) with ((proj1_sig w / ((2#1) * (inject_Z (Z.pos n))))) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field; unfold Qeq; simpl; auto with *). rewrite -> Qabs_pos;[apply Qle_refl|]. apply Qle_shift_div_l. rewrite <- (Qmult_0_r (2#1)). apply Qmult_lt_l. reflexivity. simpl; auto with *; unfold Qlt; simpl; auto with *. rewrite Qmult_0_l. exact (Qpos_nonneg w). destruct H0. apply Qle_antisym; auto. eapply Z.le_trans;[|apply Z.le_max_r]. unfold rasterize1. rewrite <- (Qfloor_Z (Z.pos n -1)). apply Qfloor_resp_le. setoid_replace x with (l+proj1_sig w). setoid_replace (l + proj1_sig w - l) with (proj1_sig w) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). unfold Qdiv. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. 2: apply Qpos_nonzero. rewrite <- Zle_Qle. rewrite <- (Z.add_0_r (Z.pos n)) at 2. apply Z.add_le_mono_l. discriminate. apply Qle_antisym. apply H0. exact q. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround