proposition: Lemma RasterizeQ2_correct2 : forall (x y : Q), @InFinEnumC (ProductMS _ _) (x,y) (CentersOfPixels (PixelizeQ2 (RasterizeQ2 points n m t l b r)) (l,t) (r,b)) -> exists p, In p points /\ ball (proj1_sig err) p (x,y).
proof: Proof. intros x y H. apply InFinEnumC_Qepsilon in H. destruct H as [q [qin qeq]]. destruct q as [qx qy]. destruct (InterpRaster_correct2 _ _ _ _ _ _ _ (RasterizeQ2_wf points n m t l b r) qin) as [[j i] [Hij [Hx' Hy']]]. unfold fst, snd in Hij. apply RasterizeQ2_in_recip in Hij. 2: apply emptyRaster_wf. destruct Hij. 2: unfold Is_true in H; rewrite (emptyRasterEmpty n m j i) in H; contradiction. unfold RasterizeQ2 in H. rewrite map_map in H. apply In_nth with (d:=(fun x : Q * Q => (Z.to_nat (fst (rasterize2 n m t l b r x)), Z.to_nat (snd (rasterize2 n m t l b r x))))(0,0)) in H. destruct H as [k [kin H]]. rewrite map_length in kin. rewrite (map_nth (fun x : Q * Q => (Z.to_nat (fst (rasterize2 n m t l b r x)), Z.to_nat (snd (rasterize2 n m t l b r x))))) in H. exists (nth k points (0,0)). split. apply nth_In. exact kin. unfold snd in Hx'. unfold fst in Hy'. assert (Z.to_nat (fst (rasterize2 n m t l b r (nth k points (0, 0)))) = j /\ Z.to_nat (snd (rasterize2 n m t l b r (nth k points (0, 0)))) = i). { inversion H. split; reflexivity. } clear H. destruct H0. rewrite <- qeq. clear qeq x y. specialize (@Hf (fst (nth k points (0,0))) (snd (nth k points (0,0)))). rewrite <- surjective_pairing in Hf. specialize (@Hf (InFinEnumC_weaken _ _ points (nth_In _ _ kin))). split. - unfold rasterize2, snd in H0. clear H. simpl (fst (qx,qy)). rewrite Hx', <- H0. rewrite Z2Nat.id. apply ball_weak_le with (e:=((1 # 2 * n) * proj1_sig w)). apply (Qpos_max_ub_l errX errY). apply ball_sym. apply rasterize1_error. apply Hf. apply rasterize2_bound. - unfold rasterize2, fst in H. clear H0 Hx'. simpl (snd (qx,qy)). rewrite Hy', <- H. 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 _ (proj2 Hf)). rewrite <- switch_line_interp in H0. apply ball_sym. rewrite Z2Nat.id. apply H0. apply Z.le_0_sub, Z.le_min_l. apply (Z.le_lt_trans _ _ _ (Z.le_min_l _ _)). rewrite <- (Z.add_0_r (Z.pos m)) at 2. apply Z.add_lt_mono_l. reflexivity. 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