proposition: Lemma ProductMinLimits : forall { I J : IntegrationSpace } (f : PartialFunction (X (ProductFunctionRieszSpace I J))) (fL : L (ProductFunctionRieszSpace I J) f), CR_cv _ (fun n : nat => IElemProduct (XminConst f (INR n)) (LminIntStable n f fL)) (IElemProduct f fL) * CR_cv _ (fun n : nat => IElemProduct (XminConst (Xabs f) (CR_of_Q _ (1 # Pos.of_nat (S n)))) (LminConstStable (CR_of_Q _ (1 # Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable (ProductFunctionRieszSpace I J) f fL))) 0.
proof: Proof. intros. split. - destruct fL as [l fL]. destruct (CRup_nat (fold_right (CRplus _) 0 (map (fun a => CRabs _ (prodint_factor a)) l))) as [n nup]. exists n. intros. setoid_replace (IElemProduct (XminConst f (INR i)) (LminIntStable i f (existT (fun l0 : list ProdIntegrable => PartialRestriction (ProdLFunc l0) f) l fL)) - IElemProduct f (existT (fun l0 : list ProdIntegrable => PartialRestriction (ProdLFunc l0) f) l fL)) with (CR_of_Q (RealT (ElemFunc I)) 0). rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. rewrite <- (CRplus_opp_r (IElemProduct f (existT (fun l0 : list ProdIntegrable => PartialRestriction (ProdLFunc l0) f) l fL))). apply CRplus_morph. 2: reflexivity. symmetry. apply IElemProductExtensional. intros. unfold XminConst, Xop, partialApply. rewrite CRmin_left. destruct fL. rewrite (c x xD (d x xD)). apply DomainProp. simpl in yD. destruct fL. rewrite <- (c x xD). apply (CRle_trans _ _ _ (applyProdLFuncBound l x xD)). apply (CRle_trans _ (CR_of_Q _ (Z.of_nat n # 1))). apply CRlt_asym, nup. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, H. - apply ProductMinLimitDecr. intros x xdf. apply CRabs_pos. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile