proposition: Lemma ProductMinLimitDecr : forall { I J : IntegrationSpace } (g : PartialFunction (X (ProductFunctionRieszSpace I J))) (gL : L (ProductFunctionRieszSpace I J) g), nonNegFunc g -> CR_cv _ (fun n : nat => IElemProduct (XminConst g (CR_of_Q _ (1 # Pos.of_nat (S n)))) (LminConstStable (CR_of_Q _ (1 # Pos.of_nat (S n))) g (invSuccRealPositive n) gL)) 0.
proof: Proof. intros. destruct gL as [l res]. assert (forall n:nat, IElemProduct (ProdLFunc (map (ProdIntegrableMapCoef (fun x => CRmin x (CR_of_Q _ (1 # Pos.of_nat (S n))))) (ProdIntegrableSimplify l))) (existT _ (map (ProdIntegrableMapCoef (fun x => CRmin x (CR_of_Q _ (1 # Pos.of_nat (S n))))) (ProdIntegrableSimplify l)) (PartialRestriction_refl _ _)) == IElemProduct (XminConst g (CR_of_Q _ (1 # Pos.of_nat (S n)))) (LminConstStable (CR_of_Q _ (1 # Pos.of_nat (S n))) g (invSuccRealPositive n) (existT (fun l0 : list ProdIntegrable => PartialRestriction (ProdLFunc l0) g) l res))). { intro n. apply IElemProductExtensional. intros. destruct (ProductMinConstStable l (CR_of_Q _ (1 # Pos.of_nat (S n))) (invSuccRealPositive n)). rewrite (c x xD (d x xD)). unfold XminConst, Xop, partialApply. destruct res. rewrite (c0 x (d x xD) yD). reflexivity. } apply (CR_cv_eq _ (fun n => IElemProduct (ProdLFunc (map (ProdIntegrableMapCoef (fun x => CRmin x (CR_of_Q _ (1 # Pos.of_nat (S n))))) (ProdIntegrableSimplify l))) (existT _ (map (ProdIntegrableMapCoef (fun x => CRmin x (CR_of_Q _ (1 # Pos.of_nat (S n))))) (ProdIntegrableSimplify l)) (PartialRestriction_refl _ _)))). exact H0. apply (seq_cv_0_bound _ (fun n => CR_of_Q _ (1 # Pos.of_nat (S n)) * fold_right (CRplus (RealT (ElemFunc I))) 0 (map (fun pi : ProdIntegrable => MeasureSet (prodint_fint pi) * CRcast (MeasureSet (prodint_gint pi))) (ProdIntegrableSimplify l)))). - intro n. rewrite H0. destruct (LminConstStable (CR_of_Q _ (1 # Pos.of_nat (S n))) g (invSuccRealPositive n) (existT (fun l0 : list ProdIntegrable => PartialRestriction (ProdLFunc l0) g) l res)). rewrite IElemProductFubini. apply IntegralNonNeg. intros x0 xdf. simpl. apply (@IntegralNonNeg (IntegrationSpaceCast J)). intros x1 xdf0. simpl. destruct p. rewrite (c _ xdf0 (d _ xdf0)). apply CRmin_glb. apply H. apply CR_of_Q_le. discriminate. - intro n. generalize (ProdIntegrableSimplify l). induction l0. simpl (fold_right (CRplus _) 0 (map (fun pi : ProdIntegrable => MeasureSet (prodint_fint pi) * MeasureSet (prodint_gint pi)) nil)). rewrite CRmult_0_r. apply CRle_refl. simpl (fold_right (CRplus _) 0 (map (fun pi : ProdIntegrable => MeasureSet (prodint_fint pi) * CRcast (MeasureSet (prodint_gint pi))) (a :: l0))). rewrite CRmult_plus_distr_l. apply CRplus_le_compat. 2: exact IHl0. destruct a; unfold prodint_gint, prodint_fint, ProdIntegrableMapCoef, prodint_factor, prodint_gint, prodint_fint. rewrite CRmult_assoc. apply CRmult_le_compat_r. rewrite <- (CRmult_0_l (CRcast (MeasureSet prodint_gint0))). apply CRmult_le_compat_r. unfold CRcast. rewrite <- (CRmorph_zero (@SlowConstructiveRealsMorphism (RealT (ElemFunc J)) (RealT (ElemFunc I)))). apply CRmorph_le. apply MeasureNonNeg. apply MeasureNonNeg. apply CRmin_r. - apply seq_cv_0_mult. intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. 2: discriminate. apply (Nat.le_trans _ _ _ H1). apply le_S, Nat.le_refl. apply CR_of_Q_le. discriminate. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile