proposition: Lemma Cmap_slow_wd_loc : forall (X Y : MetricSpace) (f g : X --> Y) (x : Complete X) (e : Qpos), (forall a : X, ball (proj1_sig e) (Cunit a) x -> msp_eq (f a) (g a)) -> @msp_eq _ (Cmap_slow_fun f x) (Cmap_slow_fun g x).
proof: Proof. intros. intros e1 e2. simpl. unfold Cmap_slow_raw; simpl. pose (QposInf_min (Qpos2QposInf (1#2)*(mu g e2)) (QposInf_min (Qpos2QposInf (1#2)*(mu f e1)) e)) as d. rewrite Qplus_0_r. apply (ball_triangle _ (proj1_sig e1) (proj1_sig e2) _ (f (approximate x d))). - apply (uc_prf f). destruct (mu f e1). 2: reflexivity. simpl. destruct d eqn:des. assert (Qle (proj1_sig q0) ((1 # 2) * proj1_sig q)). { pose proof (QposInf_min_lb_r (Qpos2QposInf (1 # 2) * mu g e2) (QposInf_min (Qpos2QposInf (1 # 2) * q) e)). subst d. rewrite des in H0. simpl in H0. apply (Qle_trans _ _ _ H0), Qpos_min_lb_l. } apply (Qplus_le_l _ _ ((1#2)*proj1_sig q)) in H0. ring_simplify in H0. rewrite Qplus_comm in H0. apply (ball_weak_le _ _ _ H0). apply (regFun_prf x ((1#2)*q)%Qpos q0). exfalso. subst d. destruct (mu g e2); discriminate. - rewrite H. + apply (uc_prf g). destruct (mu g e2). 2: reflexivity. simpl. destruct d eqn:des. assert (Qle (proj1_sig q0) ((1 # 2) * proj1_sig q)). { pose proof (QposInf_min_lb_l (Qpos2QposInf (1 # 2) * q) (QposInf_min (Qpos2QposInf (1 # 2) * mu f e1) e)). subst d. rewrite des in H0. exact H0. } apply (Qplus_le_l _ _ ((1#2)*proj1_sig q)) in H0. ring_simplify in H0. apply (ball_weak_le _ _ _ H0). apply (regFun_prf x q0 ((1#2)*q)%Qpos). exfalso. subst d. destruct (mu f e1); discriminate. + destruct d eqn:des. assert (proj1_sig q <= proj1_sig e). { destruct (Qpos2QposInf (1 # 2) * mu g e2)%QposInf. destruct (Qpos2QposInf (1 # 2) * mu f e1)%QposInf. simpl in d. subst d. inversion des. apply (Qle_trans _ (proj1_sig (Qpos_min q1 e))). apply Qpos_min_lb_r. apply Qpos_min_lb_r. subst d. simpl in des. inversion des. apply Qpos_min_lb_r. simpl in d. subst d. destruct (mu f e1). simpl in des. inversion des. apply Qpos_min_lb_r. simpl in des. inversion des. apply Qle_refl. } apply (ball_weak_le _ _ _ H0). apply ball_approx_l. exfalso. destruct (mu g e2), (mu f e1); discriminate. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax