proposition: Lemma IntegralRepresentationShiftVal : forall {IS : IntegrationSpace} (fInt : @IntegralRepresentation IS) (n : nat), IntegralSeries (IntegralRepresentationShift fInt n) == IntegralSeries fInt - CRsum (fun k => I IS _ (IntFnL fInt k)) n.
proof: Proof. intros. apply (series_cv_unique (fun n0 : nat => I IS (IntFn (IntegralRepresentationShift fInt n) n0) (IntFnL (IntegralRepresentationShift fInt n) n0))). exact (IntegralCv (IntegralRepresentationShift fInt n)). simpl. apply (CR_cv_eq _ (fun k => CRsum (fun n0 : nat => I IS _ (IntFnL fInt n0)) (S n + k) - CRsum (fun k : nat => I IS (IntFn fInt k) (IntFnL fInt k)) n)). intros. rewrite sum_assoc. simpl. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. apply CR_cv_minus. 2: apply CR_cv_const. intro p. pose proof (IntegralCv fInt p) as [k kmaj]. exists k. intros. apply kmaj. apply (Nat.le_trans _ (0+i) _ H). apply Nat.add_le_mono_r, Nat.le_0_l. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions