proposition: Lemma RasterizeQ2_correct1 : forall (x y:Q), @InFinEnumC (ProductMS _ _) (x,y) points -> exists p, In p (CentersOfPixels (PixelizeQ2 (RasterizeQ2 points n m t l b r)) (l,t) (r,b)) /\ ball (proj1_sig err) p (x,y).
proof: Proof. intros x y H. pose proof (Hf H) as xybound. apply InFinEnumC_Qepsilon in H. destruct H as [q [H H0]]. assert (let (i,j) := rasterize2 n m t l b r q in Is_true (RasterIndex (PixelizeQ2 (RasterizeQ2 points n m t l b r)) (Z.to_nat i) (Z.to_nat j))). { apply RasterizeQ2_in. apply (in_map (fun p : Q * Q => rasterize2 n m t l b r p) points). exact H. apply emptyRaster_wf. apply Nat2Z.inj_lt. rewrite positive_nat_Z, Z2Nat.id. apply Z.lt_0_sub. ring_simplify. apply (Z.lt_le_trans _ (0+1)). reflexivity. apply Z.add_le_mono_r. apply rasterize2_bound. apply Z.le_0_sub. apply Z.le_min_l. apply Nat2Z.inj_lt. rewrite positive_nat_Z, Z2Nat.id. apply rasterize2_bound. apply rasterize2_bound. } pose (Z.pos m - 1 - Z.min (Z.pos m - 1) (Z.max 0 (rasterize1 b t m (snd q))))%Z as i. pose (Z.min (Z.pos n - 1) (Z.max 0 (rasterize1 l r n (fst q)))) as j. exists ((fun (l r : Q) (n : positive) (i : Z) => l + (r - l) * (2 * i + 1 # 1) / (2 * Z.pos n # 1)) l r n (Z.of_nat (Z.to_nat j)), (fun (l r : Q) (n : positive) (i : Z) => l + (r - l) * (2 * i + 1 # 1) / (2 * Z.pos n # 1)) t b m (Z.of_nat (Z.to_nat i))). split. apply InterpRaster_correct1. apply RasterizeQ2_wf. exact H1. rewrite Z2Nat.id. rewrite Z2Nat.id. destruct H0, q. split. - unfold fst. destruct xybound. apply Qball_0 in H0. unfold fst in H0. clear H2. rewrite <- H0 in H3. unfold j, r. rewrite <- H0. unfold fst. apply ball_weak_le with (e:=((1 # 2 * n) * proj1_sig w)). apply (Qpos_max_ub_l errX errY). apply (@rasterize1_error l w n _ H3). - unfold snd. destruct xybound. apply Qball_0 in H2. unfold snd in H2. clear H0. rewrite <- H2 in H4. unfold i, t. rewrite <- H2. unfold snd. apply ball_weak_le with (e:=((1 # 2 * m) * proj1_sig h)). apply (Qpos_max_ub_r errX errY). pose proof (@rasterize1_error b h m _ H4). rewrite <- switch_line_interp in H0. apply H0. apply rasterize2_bound. - unfold i. apply Z.le_0_sub. apply Z.le_min_l. - apply rasterize2_bound. 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