proposition: Lemma CompactIntervalQ_prf : is_RegularFunction (@ball (FinEnum Q_as_MetricSpace)) CompactIntervalQ_raw.
proof: Proof. cut (forall (e1 e2:Qpos), hemiMetric Q_as_MetricSpace (proj1_sig e1 + proj1_sig e2) (fun a : Q_as_MetricSpace => InFinEnumC a (CompactIntervalQ_raw e1)) (fun a : Q_as_MetricSpace => InFinEnumC a (CompactIntervalQ_raw e2))). { intros Z e1 e2. split. apply (Qpos_nonneg (e1+e2)). split. apply Z. eapply hemiMetric_wd1;[|apply Z]. unfold QposEq; simpl; ring. } intros e1 e2 a Ha. assert (l <= a <= r). { unfold CompactIntervalQ_raw in Ha. set (e1':=Z.to_pos (Qceiling ((r - l) / (inject_Z 2 * proj1_sig e1)))) in *. assert (L:=UniformPartition_inside e1'). induction (UniformPartition e1'). exfalso; exact (FinSubset_ball_nil Ha). destruct (Qeq_dec a a0) as [A|A]. rewrite -> A. auto with *. apply IHl0; auto with *. apply FinSubset_ball_orC in Ha. destruct Ha as [G | Ha | Ha] using orC_ind. intro abs. contradict G; intro G. contradiction. elim A. apply Qball_0 in Ha. exact Ha. assumption. } unfold CompactIntervalQ_raw. set (e2':=Z.to_pos (Qceiling ((r - l) / (inject_Z 2 * proj1_sig e2)))). pose proof (UniformPartition_fine e2' H) as [y [Hy0 Hy1]]. apply existsWeaken. exists y. split. - apply InFinEnumC_weaken, Hy0. - simpl. rewrite -> Qball_Qabs. eapply Qle_trans;[apply Hy1|]. apply Qle_trans with (proj1_sig e2). apply Qle_shift_div_r. destruct e2'; auto with *. rewrite Qmult_comm, (Qmult_comm (2#1)), <- Qmult_assoc. rewrite <- (Qinv_involutive (inject_Z 2*proj1_sig e2)). apply Qle_shift_div_l. + apply Qinv_lt_0_compat. exact (Qpos_ispos ((2#1)*e2)). + unfold e2'. generalize (CompactIntervalQ_nat e2). unfold Qdiv. generalize ((r - l) * / (inject_Z 2 * proj1_sig e2)). intros q He. apply Qle_trans with (inject_Z (Qceiling q)). apply Qle_ceiling. destruct (Qceiling q). discriminate. rewrite Z2Pos.id. apply Z.le_refl. reflexivity. discriminate. + rewrite <- Qplus_0_l at 1. apply Qplus_le_l. apply Qpos_nonneg. 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