proposition: Lemma stepSampleDistanceToId : (forall p, QposEq (@SupDistanceToLinear (stepSample p) 0 1 (@pos_one _)) (1#(2*p))).
proof: Proof. unfold QposEq. induction p using positive_rect2. replace (stepSample (xI p)) with (glue (Build_OpenUnit (oddGluePoint p)) (constStepF (Pos.succ p#xI p:QS) * (stepSample (Pos.succ p))) ((constStepF (1#(xI p):QS))*(constStepF (Pos.succ p:QS) + constStepF (p:QS)*(stepSample p)))) by (symmetry;apply: positive_rect2_red1). rewrite -> SupDistanceToLinear_glue. generalize (@affineCombo_gt (OpenUnitDual (Build_OpenUnit (oddGluePoint p))) 0 1 (pos_one Q_as_COrdField)) (@affineCombo_lt (OpenUnitDual (Build_OpenUnit (oddGluePoint p))) 0 1 (pos_one Q_as_COrdField)). intros A B. set (C:=(pos_one Q_as_COrdField)) in *. transitivity (Qmax (1#2*xI p) (1#2*xI p))%Q;[|apply Qmax_idem]. apply Qmax_compat. set (LHS := (SupDistanceToLinear (constStepF (X:=QS) (Pos.succ p # xI p) * stepSample (Pos.succ p)) A)). transitivity ((Pos.succ p#xI p)*proj1_sig (SupDistanceToLinear (stepSample (Pos.succ p)) C))%Q; [|rewrite -> IHp; change ((Pos.succ p * 1 * (2 * (2* p + 1)) = 2* (Pos.succ p + p * (2* (Pos.succ p))))%Z); repeat rewrite Zpos_succ_morphism; ring]. assert (X:(Pos.succ p # xI p) *0 < (Pos.succ p # xI p) *1). constructor. rewrite -> (fun a => SupDistanceToLinear_scale a C X). apply SupDistanceToLinear_wd1. simpl; ring. unfold affineCombo; simpl; ring. set (LHS := (SupDistanceToLinear (constStepF (X:=QS) (1 # xI p) * (constStepF (X:=QS) (Pos.succ p) + constStepF (X:=QS) p * stepSample p)) B)%Q). transitivity ((1#xI p)*(p*proj1_sig (SupDistanceToLinear (stepSample (p)) C)))%Q; [|rewrite -> IHp0; change ((p * 1 * (2 * (2* p + 1)) = 2* (p + p * (2* p)))%Z); ring]. assert (X0:(p *0 < p *1)). constructor. rewrite -> (fun a => SupDistanceToLinear_scale a C X0). assert (X1:(p*0 + Pos.succ p < p*1 + Pos.succ p)). apply: plus_resp_less_rht. assumption. rewrite -> (fun a => SupDistanceToLinear_translate a X0 X1). assert (X2:((1# xI p)*(p*0 + Pos.succ p) < (1#xI p)*(p*1 + Pos.succ p))). apply: mult_resp_less_lft;simpl; auto with *. rewrite -> (fun a => SupDistanceToLinear_scale a X1 X2). apply SupDistanceToLinear_wd1. unfold affineCombo; simpl. repeat rewrite -> Zpos_succ_morphism; repeat rewrite -> Qmake_Qdiv; repeat rewrite -> Zpos_xI; field; auto with *. change (2*(p*1) + 1 = ((p*1*1 + Pos.succ p*1)*1))%Z. rewrite Zpos_succ_morphism; ring. change (1#2*xO p)%Q with ((1#2)*(1#(2*p)))%Q. replace (stepSample (xO p)) with (glue (ou (1#2)) (constStepF (1#2:QS) * (stepSample p)) (constStepF (1#2:QS) * (constStepF (1:QS) + (stepSample p)))) by (symmetry;apply: positive_rect2_red2). rewrite -> SupDistanceToLinear_glue. generalize (@affineCombo_gt (OpenUnitDual (ou (1#2))) 0 1 (pos_one Q_as_COrdField)) (@affineCombo_lt (OpenUnitDual (ou (1#2))) 0 1 (pos_one Q_as_COrdField)). intros A B. set (C:=(pos_one Q_as_COrdField)) in *. transitivity (Qmax ((1#2)*(1#2 * p)) ((1#2)*(1#2 * p)))%Q;[|apply Qmax_idem]. set (D1:=(SupDistanceToLinear (constStepF (X:=QS) (1 # 2) * stepSample p) A)). set (D2:=(SupDistanceToLinear (constStepF (X:=QS) (1 # 2) * (constStepF (X:=QS) 1 + stepSample p)) B)). rewrite <- IHp. apply Qmax_compat. assert (X:((1#2) *0 < (1#2) *1)). constructor. rewrite -> (fun a c => SupDistanceToLinear_scale a c X). apply SupDistanceToLinear_wd1; constructor. assert (X0:0 + 1 < 1 +1). constructor. rewrite -> (fun a c => SupDistanceToLinear_translate a c X0). assert (X1:(1#2)*(0 + 1) < (1#2)*(1 +1)). constructor. rewrite -> (fun a => SupDistanceToLinear_scale a X0 X1). apply SupDistanceToLinear_wd1; constructor. reflexivity. 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