fact: Definition stepSample : positive -> StepQ := positive_rect2 (fun _ => StepQ) (fun p rec1 rec2 => glue (Build_OpenUnit (oddGluePoint p)) (constStepF (Pos.succ p#xI p:QS) * rec1) ((constStepF (1#(xI p):QS))*(constStepF (Pos.succ p:QS) + constStepF (p:QS)*rec2))) (fun p rec => glue (ou (1#2)) (constStepF (1#2:QS) * rec) (constStepF (1#2:QS) * (constStepF (1:QS) + rec))) (constStepF (1#2:QS)).
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