proposition: Lemma distmapmap: forall X Y (f : UniformlyContinuousSpace X Y), (ucEq (uc_compose (dist) (Map_uc (@Cmap_slow _ _ f))) (uc_compose (Cmap_slow (Map_uc f)) (dist))).
proof: Proof. pose (exist (Qlt 0) (1#2) eq_refl) as half. intros. intro x. induction x. intros e e1. simpl. unfold dist_raw. simpl. rewrite Qplus_0_r. change (ballS Y (proj1_sig e + proj1_sig e1) (Cmap_slow_raw f x e) (f (approximate x (QposInf_bind (fun y' : Qpos => (half * y')%Qpos) (mu f e1))))). unfold Cmap_slow_raw. simpl. set (ee:=(QposInf_bind (fun y' : Qpos => (half * y')%Qpos) (mu f e))). set (ee1:=(QposInf_bind (fun y' : Qpos => (half * y')%Qpos) (mu f e1))). rewrite <- ball_Cunit. assert (H:ball (m:=(Complete Y)) (proj1_sig e + proj1_sig e1) ((Cmap_slow f) (Cunit (approximate x ee))) ((Cmap_slow f) (Cunit (approximate x ee1)))). apply ball_triangle with (Cmap_slow f x);apply: (uc_prf (Cmap_slow f));[apply: ball_ex_approx_l|apply: ball_ex_approx_r]. apply H. intros e1 e2. simpl. unfold dist_raw. simpl. rewrite -> (@StepFSupBallGlueGlue Y (proj1_sig e1+0+proj1_sig e2) o (Map (fun z : RegularFunction (ball (m:=Y)) => approximate z e1) (Map (Cmap_slow_fun f) x1)) (Map (fun z : RegularFunction (ball (m:=Y)) => approximate z e1) (Map (Cmap_slow_fun f) x2)) (Map f (Map (fun z : RegularFunction (ball (m:=X)) => approximate z (QposInf_bind (fun y' : Qpos => ((1 # 2) * y')%Qpos) (mu f e2))) x1)) (Map f (Map (fun z : RegularFunction (ball (m:=X)) => approximate z (QposInf_bind (fun y' : Qpos => ((1 # 2) * y')%Qpos) (mu f e2))) x2))). split; revert e1 e2 ; [apply IHx1|apply IHx2]. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionMonad CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.metric2.Complete CoRN.model.metric2.LinfMetricMonad CoRN.metric2.StepFunctionSetoid CoRN.tactics.Qauto