proposition: Lemma ComposeContinuous_prf (f:Q_as_MetricSpace --> CR) : is_UniformlyContinuousFunction (ComposeContinuous_raw f) (mu f).
proof: Proof. intros e a b. revert a b e. apply: StepF_ind2. intros s s0 t t0 Hs Ht H e H0. apply StepF_eq_equiv in Ht. rewrite <- Ht. apply StepF_eq_equiv in Hs. rewrite <- Hs. apply H. destruct (mu f e). 2: constructor. simpl. rewrite Hs, Ht. exact H0. intros x y e H. change (ball (proj1_sig e) (f x) (f y)). apply uc_prf. destruct (mu f e); try solve [constructor]. simpl. assumption. intros o s s0 t t0 H0 H1 e H. unfold ComposeContinuous_raw in *. repeat rewrite -> MapGlue, dist_glue. intros d1 d2. apply ball_weak_le with (proj1_sig (((1#2)*((1#2)*d1)) + e + ((1#2)*((1#2)*d2)))%Qpos). simpl. Qauto_le. simpl. unfold Cap_slow_raw. simpl. rewrite -> StepFSupBallGlueGlue. split. setoid_replace ((1 # 2) * ((1 # 2) * proj1_sig d1) + proj1_sig e + (1 # 2) * ((1 # 2) * proj1_sig d2))%Q with (proj1_sig ((1 # 2) * ((1 # 2) * d1) + e + (1 # 2) * ((1 # 2) * d2))%Qpos) by (simpl; ring). apply (H0 e). destruct (mu f e); try constructor. simpl in H. rewrite -> StepFSupBallGlueGlue in H; tauto. setoid_replace ((1 # 2) * ((1 # 2) * proj1_sig d1) + proj1_sig e + (1 # 2) * ((1 # 2) * proj1_sig d2))%Q with (proj1_sig ((1 # 2) * ((1 # 2) * d1) + e + (1 # 2) * ((1 # 2) * d2))%Qpos) by (simpl; ring). apply (H1 e). destruct (mu f e); try constructor. simpl in H. rewrite -> StepFSupBallGlueGlue in H; tauto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad