proposition: Lemma id01_prf : is_RegularFunction (@ball LinfStepQ) (id01_raw:QposInf -> LinfStepQ).
proof: Proof. intros a b. unfold id01_raw. apply ball_weak_le with (proj1_sig ((1#2*(id01_raw_help a)) + (1#2*(id01_raw_help b)))%Qpos). apply: plus_resp_leEq_both; apply id01_raw_help_le. simpl (ball (m:=LinfStepQ)). pose proof stepSampleDistanceToId. assert (QposEq ((1 # 2 * id01_raw_help a) + (1 # 2 * id01_raw_help b)) ((SupDistanceToLinear (stepSample (id01_raw_help a)) (pos_one Q_as_COrdField)) + (SupDistanceToLinear (stepSample (id01_raw_help b)) (pos_one Q_as_COrdField)))). { unfold QposEq. simpl. unfold QposEq in H. simpl in H. do 2 rewrite H. reflexivity. } unfold QposEq in H0. rewrite H0. apply SupDistanceToLinear_trans. 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