proposition: Lemma CountableIntersectionIsFull : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (A : X (ElemFunc IS) -> Type), (forall x : X (ElemFunc IS), (forall n:nat, Domain (fn n) x) -> A x) -> almost_everywhere A.
proof: Proof. intros IS fn fnInt A inc. pose (fun n => IntFn (let (df,_) := countable_representation IS (fn n) (fnInt n) n in df)) as fnk. exists (XinfiniteSumAbs (diagSeq fnk)). split. - pose (fun n => IntFnL (let (df,_) := countable_representation IS (fn n) (fnInt n) n in df)) as fnkL. destruct (series_cv_maj (fun n => IntAbsSum (let (df,_) := countable_representation IS (fn n) (fnInt n) n in df)) (fun n => (CRpow (CR_of_Q _ (1#2)) n)) (CR_of_Q _ 2)) as [sumI cvI]. + intro n. destruct (countable_representation IS (fn n) (fnInt n) n). simpl. destruct p. rewrite CRabs_right. assumption. destruct x. simpl. apply (series_cv_nonneg (fun k : nat => Iabs (IntFn k) (IntFnL k))). intros. apply integralPositive. intros x xdf. rewrite applyXabs. apply CRabs_pos. assumption. + apply GeoHalfTwo. + assert (series_cv (fun k : nat => Iabs (diagSeq fnk k) (diagSeqL IS fnk fnkL k)) sumI) as H. apply (series_cv_eq (diagSeq (fun n k => let (fInt,g) := countable_representation IS (fn n) (fnInt n) n in Iabs (IntFn fInt k) (IntFnL fInt k)))). intro n. unfold diagSeq, diagSeqL. destruct (diagPlaneInv n). unfold fnk, fnkL. destruct (countable_representation IS (fn n0) (fnInt n0) n0). reflexivity. apply (DiagSeqInfiniteSumColPos _ (fun n => IntAbsSum (let (df,_) := countable_representation IS (fn n) (fnInt n) n in df))). intros. destruct (countable_representation IS (fn n) (fnInt n) n). apply integralPositive. intros y ydf. rewrite applyXabs. apply CRabs_pos. intro n. destruct (countable_representation IS (fn n) (fnInt n) n). destruct x. assumption. apply cvI. exists (Build_IntegralRepresentation IS (diagSeq fnk) (diagSeqL IS fnk fnkL) sumI H). apply PartialRestriction_refl. - intros xDiag xdf. apply inc. clear inc. intro n. simpl. pose proof (domainInfiniteSumAbsDiag _ fnk n xDiag xdf) as H. unfold fnk in H. destruct (countable_representation IS (fn n) (fnInt n) n) as [[fnn] [i _]]. unfold IntFn in i. apply i, H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions