proposition: Lemma IntegralRepresentationInvariantZero : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), (forall (x : X (ElemFunc IS)) (xD : Domain f x), partialApply f x xD == 0) -> Integral fInt == 0.
proof: Proof. intros. split. - apply representationPositive. intros x xdf. destruct fInt,p. rewrite (c x _ (d x xdf)). rewrite H. apply CRle_refl. - setoid_replace (Integral fInt) with (CRopp _ (IntegralSeries (IntegralRepresentationScale _ (-(1)) fInt))). rewrite <- CRopp_0. apply CRopp_ge_le_contravar. apply representationPositive. intros x xdf. destruct (IntegralRepresentationScaleInj f (-(1)) fInt). rewrite (c x xdf (d x xdf)). rewrite applyXscale, H. rewrite CRmult_0_r. apply CRle_refl. pose proof (IntegralScale f fInt (-(1))). rewrite H0. rewrite <- CRopp_mult_distr_r, CRmult_1_r, CRopp_involutive. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase