proposition: Lemma LinfAsL1_uc_prf : is_UniformlyContinuousFunction (fun (x:LinfStepQ) => (x:L1StepQ)) Qpos2QposInf.
proof: Proof. intros e. apply: StepF_ind2. simpl. intros s s0 t t0 Hs Ht H. intro H0. rewrite <- Hs, <- Ht in H0. specialize (H H0). clear H0. unfold L1Ball. apply StepF_eq_change_base_setoid in Hs. apply StepF_eq_change_base_setoid in Ht. rewrite <- (L1Distance_wd s s0 Hs t t0 Ht). exact H. intros x y Hxy. change (Qball (proj1_sig e) x y) in Hxy. rewrite -> Qball_Qabs in Hxy. apply Hxy. intros o s s0 t t0 Hst Hst0 H. simpl. unfold L1Ball. unfold L1Distance. unfold L1Norm. unfold StepQminus. change (@glue (msp_as_RSetoid Q_as_MetricSpace) o s s0) with (@glue QS o s s0). rewrite (MapGlue QminusS). change (@glue (msp_as_RSetoid Q_as_MetricSpace) o t t0) with (@glue QS o t t0). rewrite (ApGlueGlue (QminusS ^@> s) (QminusS ^@> s0)). unfold StepQabs. rewrite MapGlue. rewrite -> Integral_glue. setoid_replace (proj1_sig e) with (o*proj1_sig e + (1-o)*proj1_sig e)%Q; [| simpl; ring]. simpl in H. unfold StepFSupBall, StepFfoldProp in H. simpl in H. rewrite (MapGlue (ballS Q_as_MetricSpace (proj1_sig e))) in H. rewrite (ApGlueGlue (ballS Q_as_MetricSpace (proj1_sig e) ^@> s) (ballS Q_as_MetricSpace (proj1_sig e) ^@> s0)) in H. destruct H as [H0 H1]. apply Qplus_le_compat. repeat rewrite -> (Qmult_comm o). apply Qmult_le_compat_r; auto with *. apply Hst. assumption. repeat rewrite -> (Qmult_comm (1-o)). apply Qmult_le_compat_r; auto with *. apply Hst0. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.structures.StepQsec CoRN.metric2.Prelength CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetricMonad CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac