proposition: Lemma Cmap_wd_bounded : forall (Y : MetricSpace) (f g : Q_as_MetricSpace --> Y) (x : CR) (c : Qpos), (forall q:Q, -`c <= q <= `c -> msp_eq (f q) (g q)) -> (- ' (proj1_sig c) <= x /\ x <= ' (proj1_sig c))%CR -> msp_eq (Cmap_fun QPrelengthSpace f x) (Cmap_fun QPrelengthSpace g x).
proof: Proof. intros. setoid_replace x with (CRboundAbs c x). 2: symmetry; apply CRboundAbs_Eq; apply H0. pose (fun e => QposInf_min (mu f e) (mu g e)) as mufg. assert (∀ e : Qpos, QposInf_le (mufg e) (mu f e)). { intro e. unfold QposInf_le, mufg. destruct (mu f e). 2: trivial. simpl. destruct (mu g e). 2: apply Qle_refl. apply Qpos_min_lb_l. } pose proof (uc_prf_smaller f mufg H1). clear H1. setoid_replace f with (Build_UniformlyContinuousFunction H2). 2: apply ucEq_equiv; intro q; reflexivity. assert (∀ e : Qpos, QposInf_le (mufg e) (mu g e)). { intro e. unfold QposInf_le, mufg. destruct (mu g e). 2: trivial. simpl. destruct (mu f e). 2: apply Qle_refl. apply Qpos_min_lb_r. } pose proof (uc_prf_smaller g mufg H1). clear H1. setoid_replace g with (Build_UniformlyContinuousFunction H3). 2: apply ucEq_equiv; intro q; reflexivity. intros e1 e2. assert (forall y, eq (QposInf_bind (fun e : Qpos => e) y) y) as elim_bind. { intro y. destruct y; reflexivity. } simpl. rewrite elim_bind, elim_bind. clear elim_bind. assert (forall a, Qmax (- ` c) (Qmin (` c) a) <= ` c). { intro a. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } rewrite Qplus_0_r. destruct (mufg e1) as [q|] eqn:des. - rewrite H. apply (mu_sum QPrelengthSpace e2 (cons e1 nil) (Build_UniformlyContinuousFunction H3)). simpl. rewrite des. simpl. destruct (mufg e2) eqn:des2. simpl. apply AbsSmall_Qabs. apply (Qle_trans _ (Qabs (approximate x q - approximate x q0))). apply QboundAbs_contract. apply AbsSmall_Qabs. apply (regFun_prf x). simpl. trivial. split. apply Qmax_ub_l. apply H1. - rewrite <- H. apply (mu_sum QPrelengthSpace e2 (cons e1 nil) f). simpl. unfold mufg in des. destruct (mu f e1) as [q|]. exfalso. simpl in des. destruct (mu g e1); inversion des. simpl. trivial. split. apply Qmax_ub_l. apply H1. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.reals.fast.CRArith Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax MathClasses.interfaces.canonical_names MathClasses.interfaces.additional_operations