proposition: Lemma MeasurableGen : forall {IS : IntegrationSpace} (h : PartialFunction (X (ElemFunc IS))), (forall (A : (X (ElemFunc IS)) -> Prop) (Aint : IntegrableSet A) (k : positive) (eps : CRcarrier (RealT (ElemFunc IS))) (epsPos : 0 < eps), { B : SetApprox A Aint eps & IntegrableFunction (XmaxConst (XminConst (Xmult (CharacFunc (sa_approx _ _ _ B)) h) (CR_of_Q _ (Z.pos k # 1))) (CR_of_Q _ (Z.neg k # 1))) }) -> MeasurableFunction h.
proof: Proof. intros IS f fMes A n Aint. pose (fun S Sint eps epsPos => let (B,_) := fMes S Sint n eps epsPos in B) as gen. pose (fun k:nat => match k with | O => let (U,_):=IntegrableApproxSequence gen A Aint O in U | S i => let (U,Uint):=IntegrableApproxSequence gen A Aint i in sa_approx _ _ _ (gen _ (IntegrableSetDifference A U Aint Uint) (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) k) (CRpow_gt_zero (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) k (CR_of_Q_pos (1 # 2) eq_refl))) end) as Bk. assert (forall k:nat, IntegrableSet (Bk k)) as BkInt. { intro k. unfold Bk. destruct k. - destruct (IntegrableApproxSequence gen A Aint 0). exact i. - destruct (IntegrableApproxSequence gen A Aint k). apply sa_bint. } assert (forall k:nat, Integral (BkInt (S k)) <= CRpow (CR_of_Q _ (1 # 2)) k) as BkMaj. { intro k. pose proof (IntegrableApproxSequenceBound gen A Aint k). pose proof (IntegrableApproxSequenceInc gen A Aint k). destruct (IntegrableApproxSequence gen A Aint k) as [U Uint] eqn:des. apply (CRle_trans _ (MeasureSet (IntegrableSetDifference A U Aint Uint))). apply IntegralNonDecreasing. intros x xdf xdg. simpl. simpl in xdf. destruct xdf. rewrite des in y. destruct xdg. apply CRle_refl. contradict n0. exact (sa_inc _ _ _ _ x y). destruct xdg. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. rewrite MeasureDifferenceIncluded. apply CRlt_asym, X. intros. exact (H x H0). } pose (fun k:nat => (XmaxConst (XminConst (Xmult (CharacFunc (Bk k)) f) (CR_of_Q (RealT (ElemFunc IS)) (Z.pos n # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg n # 1)))) as fk. assert (forall k:nat, IntegrableFunction (fk k)) as fkInt. { unfold fk, Bk. intro k. destruct k. - simpl. unfold gen. destruct (fMes A Aint n 1 (CRzero_lt_one (RealT (ElemFunc IS)))), x; apply i. - destruct (IntegrableApproxSequence gen A Aint k) as [U Uint]. unfold gen. destruct (fMes (fun x : X (ElemFunc IS) => A x /\ ~ U x) (IntegrableSetDifference A U Aint Uint) n (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S k)) (CRpow_gt_zero (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S k) (CR_of_Q_pos (1 # 2) eq_refl))) as [B Bint]. refine (IntegrableFunctionExtensional _ _ _ Bint). split. + intros y yD. exact yD. + intros. rewrite (DomainProp _ x xD xG). reflexivity. } assert (forall (i : nat) x (xkD : forall k:nat, Domain (CharacFunc (Bk k)) x), (let (U, _) := IntegrableApproxSequence gen A Aint i in U x) -> @CRsum (RealT (ElemFunc IS)) (fun k : nat => partialApply _ x (xkD k)) i == 1) as BkDisjoint. { induction i. - intros. simpl. destruct (xkD O). reflexivity. contradict n0. simpl. simpl in H. destruct (gen A Aint 1 (CRzero_lt_one (RealT (ElemFunc IS)))). exact H. - intros. specialize (IHi x xkD). simpl in H; destruct (IntegrableApproxSequence gen A Aint i) as [U Uint] eqn:des. destruct H. specialize (IHi H). rewrite <- (CRplus_0_r 1). simpl. simpl in IHi. rewrite IHi. clear IHi. apply CRplus_morph. reflexivity. destruct (xkD (S i)). 2: reflexivity. exfalso. unfold Bk in b. rewrite des in b. pose proof (sa_inc _ _ _ _ x b). destruct H0. contradiction. clear IHi. rewrite <- (CRplus_0_l 1). simpl. apply CRplus_morph. pose proof (sa_inc _ _ _ _ x H). destruct H0. clear H. rewrite (CRsum_eq _ (fun k => 0)), sum_const, CRmult_0_l. reflexivity. intros. destruct (xkD i0). 2: reflexivity. contradict H1. pose proof (IntegrableApproxSequenceIncr gen A Aint i0 i x H). rewrite des in H1. apply H1. clear H1. unfold Bk in b. destruct i0. destruct (IntegrableApproxSequence gen A Aint 0); exact b. simpl; destruct (IntegrableApproxSequence gen A Aint i0). right. exact b. destruct (xkD (S i)). reflexivity. contradict n0. simpl. rewrite des. exact H. } assert (forall (i j : nat) x (xkD : forall k:nat, Domain (fk k) x) (dG : Domain (Xmult (CharacFunc A) f) x), (let (U, _) := IntegrableApproxSequence gen A Aint j in U x) -> le j i -> CRsum (fun k : nat => partialApply (fk k) x (xkD k)) i == partialApply (XmaxConst (XminConst (Xmult (CharacFunc A) f) (CR_of_Q _ (Z.pos n # 1))) (CR_of_Q _ (Z.neg n # 1))) x dG) as fkDisjoint. { intros. unfold fk. rewrite (CRsum_eq _ (fun k:nat => partialApply _ x (fst (xkD k)) * partialApply (XmaxConst (XminConst f (CR_of_Q _ (Z.pos n # 1))) (CR_of_Q _ (Z.neg n # 1))) x (snd (xkD O)))). - rewrite sum_scale. rewrite (BkDisjoint i x (fun k => fst (xkD k))), CRmult_1_l. simpl. destruct dG, d. rewrite CRmult_1_l, (DomainProp f x _ d0). reflexivity. contradict n0. pose proof (IntegrableApproxSequenceInc gen A Aint j x). destruct (IntegrableApproxSequence gen A Aint j). exact (H1 H). exact (IntegrableApproxSequenceIncr gen A Aint j i x H0 H). - intros. simpl. destruct (xkD i0), d. simpl. do 2 rewrite CRmult_1_l. rewrite (DomainProp f x d0 (snd (xkD 0%nat))). reflexivity. simpl. rewrite CRmult_0_l, CRmult_0_l. rewrite CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. } destruct (series_cv_maj (fun k : nat => Integral (IntegrableAbs (fkInt k))) (fun k => match k with | O => MeasureSet (BkInt O) | S i => (CRpow (CR_of_Q _ (1 # 2)) i) end * CR_of_Q _ (Z.pos n # 1)) ((CR_of_Q _ 2 + MeasureSet (BkInt O)) * CR_of_Q _ (Z.pos n # 1))) as [l lcv]. - intro k. unfold fk. rewrite CRabs_right. apply (CRle_trans _ (Integral (IntegrableScale _ (CR_of_Q _ (Z.pos n # 1)) (BkInt k)))). apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg, d. rewrite CRmult_1_l, CRmult_1_r. apply CRabs_le. split. rewrite <- CR_of_Q_opp. setoid_replace (- (Z.pos n # 1))%Q with (Z.neg n # 1). apply CRmax_r. reflexivity. apply CRmax_lub. apply CRmin_r. apply CR_of_Q_le. discriminate. contradiction. contradiction. rewrite CRmult_0_l, CRmult_0_r. rewrite CRmin_left, CRmax_left, CRabs_right. apply CRle_refl. apply CRle_refl. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. rewrite IntegralScale, CRmult_comm. destruct k. rewrite CRmult_comm. apply CRle_refl. rewrite CRmult_comm. apply CRmult_le_compat_r. apply CR_of_Q_le. discriminate. exact (BkMaj k). apply IntegralNonNeg. intros x xdf. apply CRabs_pos. - apply series_cv_scale. apply (series_cv_shift (fun n0 : nat => match n0 with | 0%nat => MeasureSet (BkInt 0%nat) | S i => CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) i end) O); simpl. exact GeoHalfTwo. - destruct lcv. pose proof (IntegrableFunctionsComplete IS fk fkInt l s) as [rep repcv]. apply (IntegrableExtensionalAE (XinfiniteSumAbs (IntFn rep))). + exists (Xplus (CharacFunc A) (XinfiniteSumAbs (IntFn rep))). split. apply IntegrablePlus. apply Aint. exists rep. apply PartialRestriction_refl. intros. split. exact (fst H). destruct repcv, p. clear c0. specialize (d x (snd H)). destruct d as [xn d]. pose proof (xn O). destruct H0. exact d1. + pose proof (IntegrableApproxSequenceLimit gen A Aint) as [Uint Umes]. destruct (MeasureZeroAE _ (IntegrableSetDifference A _ Aint Uint)) as [h hInt]. rewrite MeasureDifferenceIncluded. rewrite Umes. unfold CRminus. apply CRplus_opp_r. intros. destruct H. pose proof (IntegrableApproxSequenceInc gen A Aint x0 x). destruct (IntegrableApproxSequence gen A Aint x0). exact (H0 H). exists (Xplus (CharacFunc (fun x : X (ElemFunc IS) => exists n : nat, let (U, _) := IntegrableApproxSequence gen A Aint n in U x)) h). split. exact (IntegrablePlus _ _ Uint (fst hInt)). intros. destruct H, hInt. specialize (n0 x d0). destruct repcv, p. rewrite (c0 x dF (d1 x dF)). clear c0. destruct d. clear n0. destruct e. apply applyInfiniteSumAbs. intro p. exists x0. intros. rewrite (fkDisjoint i0 x0 x _ dG). unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. exact H. exact H0. assert (~ A x). { intro abs. apply n0. split; assumption. } clear n1 n0 i d0 h. transitivity (CR_of_Q (RealT (ElemFunc IS)) 0). apply applyInfiniteSumAbs. apply (CR_cv_eq _ (fun _ => 0)). 2: apply CR_cv_const. intros. rewrite <- (CRmult_0_l (INR (S n0))). rewrite (CRsum_eq _ (fun _ => 0)). symmetry. apply sum_const. intros. unfold fk. simpl. destruct (domainInfiniteSumAbsIncReverse (fun k : nat => XmaxConst (XminConst (Xmult (CharacFunc (Bk k)) f) (CR_of_Q (RealT (ElemFunc IS)) (Z.pos n # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg n # 1))) x (d1 x dF) i), d. contradict H. unfold Bk in b. destruct i. pose proof (IntegrableApproxSequenceInc gen A Aint O x). destruct (IntegrableApproxSequence gen A Aint 0). exact (H b). destruct (IntegrableApproxSequence gen A Aint i). exact (proj1 (sa_inc _ _ _ _ x b)). rewrite CRmult_0_l, CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. simpl. destruct dG, d. contradiction. rewrite CRmult_0_l, CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. + exists rep. apply PartialRestriction_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile