proposition: Lemma SliceNonNegFunc : forall {R : ConstructiveReals} {X : Set} (f : @PartialFunction R X) (A : X -> Prop) (nk : nat -> nat), (forall n:nat, lt (nk n) (nk (S n))) -> nk O = O -> nonNegFunc f -> PartialRestriction (XinfiniteSumAbs (fun k : nat => Xmin (Xscale (INR (nk (S k) - nk k)) (CharacFunc A)) (Xminus f (XminConst f (INR (nk k)))))) (Xmult (CharacFunc A) f).
proof: Proof. split. - intros x [xn _]. specialize (xn O). destruct f, xn, d0, d0; split. exact d0. apply d. - intros. apply applyInfiniteSumAbs. assert (forall n:nat, Domain (Xscale (INR (nk (S n) - nk n)) (@CharacFunc R _ A)) x) as H2. { intro n. apply (domainInfiniteSumAbsIncReverse _ _ xD n). } assert (forall n:nat, Domain (Xminus f (XminConst f (INR (nk n)))) x) as H3. { intro n. apply (domainInfiniteSumAbsIncReverse _ _ xD n). } destruct xG. destruct d as [inA | notInA]. + assert (Domain f x) as H4. { specialize (H3 O). apply H3. } apply (series_cv_eq (fun n : nat => CRmin (INR (nk (S n) - nk n)) (partialApply f x H4 - CRmin (partialApply f x H4) (INR (nk n))))). intro n. rewrite (applyXmin _ _ x (H2 n) (H3 n)). apply CRmin_morph. rewrite applyXscale. rewrite (DomainProp (CharacFunc A) x _ (left inA)). unfold CharacFunc, partialApply. rewrite CRmult_1_r. reflexivity. destruct (H3 n). rewrite (applyXminus f (XminConst f (INR (nk n)))). apply CRplus_morph. apply DomainProp. apply CRopp_morph. rewrite applyXminConst. apply CRmin_morph. apply DomainProp. reflexivity. setoid_replace (partialApply (Xmult (CharacFunc A) f) x (left inA, d0)) with (partialApply f x H4). apply (@SliceBar R X). exact H. exact H0. apply H1. destruct f; simpl. rewrite CRmult_1_l. apply DomainProp. + apply (series_cv_eq (fun _ => 0)). intro n. rewrite (applyXmin _ _ x (H2 n) (H3 n)), CRmin_left. rewrite applyXscale. rewrite (DomainProp (CharacFunc A) x _ (right notInA)). unfold CharacFunc, partialApply. rewrite CRmult_0_r. reflexivity. rewrite applyXscale. rewrite (DomainProp (CharacFunc A) x _ (right notInA)). apply (CRle_trans _ 0). unfold CharacFunc, partialApply. rewrite CRmult_0_r. apply CRle_refl. destruct (H3 n). rewrite (applyXminus f (XminConst f (INR (nk n)))). apply CRle_minus. rewrite applyXminConst. rewrite (DomainProp f x d1 d). apply CRmin_l. setoid_replace (partialApply (Xmult (CharacFunc A) f) x (right notInA, d0)) with (CR_of_Q R 0). intro p. exists O. intros. rewrite sum_const, CRmult_0_l. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. clear xD. destruct f; simpl. apply CRmult_0_l. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity