proposition: Lemma INonDecreasing : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f) (gL : L (ElemFunc IS) g), (forall (x : X (ElemFunc IS)) (xF : Domain f x) (y : Domain g x), partialApply f x xF <= partialApply g x y) -> I IS f fL <= I IS g gL.
proof: Proof. intros. intro abs. destruct (Icontinuous IS (Xminus f g) (fun n:nat => Izero IS) (LminusStable f g fL gL) (fun n:nat => Izero_is_L IS) (fun n:nat => Izero_nonNeg IS)) as [[x xdminus xdfn] [l [H1 H0]]]. - exists 0. split. + intros n. exists O. intros. rewrite CRabs_right. rewrite sum_eq_R0. unfold CRminus. rewrite CRplus_opp_r. apply CR_of_Q_le. discriminate. intro k. apply Izero_is_zero. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite sum_eq_R0. apply CRle_refl. intro k. apply Izero_is_zero. + unfold Xminus. unfold LminusStable. rewrite Iadditive. rewrite Ihomogeneous. rewrite <- (CRopp_mult_distr_l 1). rewrite CRmult_1_l. rewrite <- (CRplus_opp_r (I IS g gL)). apply CRplus_lt_compat_r. exact abs. - unfold cpxF in H0. destruct xdminus. rewrite (applyXminus f g) in H0. simpl in H0. assert (series_cv (fun n : nat => partialApply (Izero IS) x (xdfn n)) 0). { apply (CR_cv_eq _ (fun n => 0)). 2: apply CR_cv_const. intro n. rewrite sum_eq_R0. reflexivity. intro k. apply applyIzero. } assert (l == 0). { apply (series_cv_unique (fun n : nat => partialApply (Izero IS) x (xdfn n))). apply H1. apply H2. } rewrite H3 in H0. clear H1 H2 H3 l. rewrite <- (CRplus_opp_r (partialApply g x d0)) in H0. apply CRplus_lt_reg_r in H0. exact (H x _ _ H0). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions