proposition: Lemma applyPlusTruncated : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (n M : nat) (x : X (ElemFunc IS)) (pF : Domain f x) (pS : Domain (Xplus (XposPart f) (if le_dec n M then Izero IS else XnegPart f)) x), partialApply _ x pS == (CRmax 0 (partialApply f x pF) + (if le_dec n M then 0 else CRmax 0 (- partialApply f x pF))).
proof: Proof. intros. destruct (le_dec n M). - rewrite CRplus_0_r. destruct pS. rewrite (applyXplus (XposPart f) (Izero IS)). unfold Izero. rewrite applyXscale, CRmult_0_l. rewrite <- (DomainProp (XposPart f) x (pF, pF)). rewrite applyXposPart. rewrite CRplus_0_r. reflexivity. - destruct pS. rewrite (applyXplus (XposPart f) (XnegPart f)). apply CRplus_morph. rewrite <- (DomainProp (XposPart f) x (pF, pF)). rewrite applyXposPart. reflexivity. rewrite <- (DomainProp (XnegPart f) x (pF, pF)). rewrite applyXnegPart. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase