proposition: Lemma MeasurableGenApprox : forall {IS : IntegrationSpace} (h : PartialFunction (X (ElemFunc IS))), almost_everywhere (Domain h) -> (forall (A : (X (ElemFunc IS)) -> Prop) (Aint : IntegrableSet A) (n : positive) (eps : CRcarrier (RealT (ElemFunc IS))) (epsPos : 0 < eps), { fB : prod (PartialFunction (X (ElemFunc IS))) (SetApprox A Aint eps) & prod (IntegrableFunction (fst fB)) (forall (x : X (ElemFunc IS)) (xdh : Domain h x) (xdf : Domain (fst fB) x), sa_approx _ _ _ (snd fB) x -> CRabs _ (partialApply (XmaxConst (XminConst h (CR_of_Q _ (Z.pos n # 1))) (CR_of_Q _ (Z.neg n # 1))) x xdh - partialApply _ x xdf) < eps) }) -> MeasurableFunction h.
proof: Proof. intros IS h dom H. apply MeasurableGen. intros A Aint k eps epsPos. specialize (H A Aint k). assert (forall (i:nat), 0 < eps * CRpow (CR_of_Q _ (1 # 2)) i) as H0. { intros. apply (CRmult_lt_0_compat _ _ _ epsPos). apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. } pose (fun (i:nat) => sa_approx _ _ _ (let (fB,_) := H (eps * CRpow (CR_of_Q _ (1#2)) (S i)) (H0 (S i)) in snd fB)) as Bi. assert ({ BI : IntegrableSet (fun x => forall i:nat, Bi i x) & MeasureSet Aint - MeasureSet BI < eps }) as Bint. { destruct (CR_cv_maj (fun n => - MeasureSet (IntegrableSetIntersectIterate _ (fun i => sa_bint _ _ _ (let (fB,_) := H (eps * CRpow (CR_of_Q _ (1 # 2)) (S i)) (H0 (S i)) in snd fB)) n)) (fun n => (CRpow (CR_of_Q _ (1 # 2)) (2 + n) * eps)) (CR_of_Q _ (1 # 2) * eps)). intro n. unfold CRminus. rewrite CRopp_involutive, CRplus_comm. pose proof (@MeasureDifferenceIncluded IS). unfold CRminus in H1. rewrite <- H1, CRabs_right. clear H1. 2: apply MeasureNonNeg. apply (CRle_trans _ (MeasureSet Aint - MeasureSet (sa_bint _ _ _ (let (fB,_) := H (eps * CRpow (CR_of_Q _ (1 # 2)) (2 + n)) (H0 (2 + n)%nat) in snd fB)))). rewrite <- MeasureDifferenceIncluded. apply MeasureNonDecreasing. intros. destruct H1. split. apply (sa_inc _ _ _ (let (fB,_) := H (eps * CRpow (CR_of_Q _ (1 # 2)) (S n)) (H0 (S n)) in snd fB)). destruct n; apply H1. intro abs. contradict H2. split; assumption. apply sa_inc. rewrite <- (CRmult_comm eps). apply CRlt_asym. apply sa_mes. clear H1. intros. apply H1. apply (series_cv_eq (fun n : nat => CRpow (CR_of_Q _ (1 # 2)) n * ((CR_of_Q _ (1 # 2)) * (CR_of_Q _ (1 # 2)) * eps))). intros. simpl. rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity. rewrite (CRmult_comm (CRpow (CR_of_Q _ (1 # 2)) n)), <- CRmult_assoc. reflexivity. apply (CR_cv_proper _ (CR_of_Q _ 2 * (CR_of_Q _ (1 # 2) * CR_of_Q _ (1 # 2) * eps))). apply series_cv_scale. exact GeoHalfTwo. rewrite <- CRmult_assoc, <- CRmult_assoc, <- (CR_of_Q_mult _ 2). setoid_replace (2 * (1#2))%Q with 1%Q. rewrite CRmult_1_l. reflexivity. reflexivity. destruct p. simpl in c0. apply CR_cv_opp in c. apply (CR_cv_eq (fun n : nat => MeasureSet (IntegrableSetIntersectIterate _ (fun i : nat => sa_bint A Aint (eps * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S i)) (let (fB, _) := H (eps * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S i)) (H0 (S i)) in snd fB)) n))) in c. destruct (IntegrableSetCountableIntersect _ _ _ c) as [intersectInt c1]. exists intersectInt. clear c. rewrite <- CRopp_involutive, <- c1 in c0. clear c1 x. apply (CRplus_le_compat_l (MeasureSet Aint)) in c0. rewrite (CRplus_comm (CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * eps)) in c0. rewrite <- CRplus_assoc in c0. apply (CRle_lt_trans _ _ _ c0). clear c0. apply (CRlt_le_trans _ (eps * (CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * 1) + CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * eps)). apply CRplus_lt_compat_r. apply sa_mes. rewrite CRmult_1_r, CRmult_comm, <- CRmult_plus_distr_r, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1 # 2))%Q with 1%Q. rewrite CRmult_1_l. apply CRle_refl. reflexivity. intro n. apply CRopp_involutive. } assert (forall (x : X (ElemFunc IS)), (forall i : nat, Bi i x) -> A x). { intros. unfold Bi in H1. exact (sa_inc _ _ _ _ x (H1 O)). } destruct Bint as [BI Bmaj]. exists (Build_SetApprox IS A Aint eps _ BI Bmaj H1). pose (fun i:nat => let (fB,_) := H (eps * CRpow (CR_of_Q _ (1#2)) (S i)) (H0 (S i)) in fst fB) as fi. assert (forall i:nat, IntegrableFunction (Xmult (CharacFunc (fun x => forall i : nat, Bi i x)) (fi i))) as fiInt. { intro i. unfold fi. destruct (H (eps * CRpow (CR_of_Q _ (1 # 2)) (S i)) (H0 (S i))). exact (RestrictedIntegrable (fst p) BI). } destruct (series_cv_maj (fun n : nat => Integral (IntegrableAbs (IntegrableMinus (fiInt (S n)) (fiInt n)))) (fun n:nat => CRpow (CR_of_Q _ (1#2)) n * (CR_of_Q _ 2 * eps * MeasureSet BI)) (CR_of_Q _ 2 * (CR_of_Q _ 2 * eps * MeasureSet BI))) as [l lcv]. - intro n. rewrite CRabs_right. destruct dom as [hdom [hdomInt dom]]. apply (CRle_trans _ (Integral (IntegrablePlus _ _ (IntegrableScale _ 0 hdomInt) (IntegrableScale _ (CR_of_Q _ 2 * (eps * CRpow (CR_of_Q _ (1 # 2)) n)) BI)))). apply IntegralNonDecreasing. intros x xdf xdg. unfold fi. unfold fi in xdf. destruct xdg as [d d0]. destruct d0. pose proof (b n) as bn. unfold Bi in bn. pose proof (b (S n)) as bSn. unfold Bi in bSn. destruct (H (eps * CRpow (CR_of_Q _ (1 # 2)) (S n)) (H0 (S n))) as [x0 p]. destruct (H (eps * CRpow (CR_of_Q _ (1 # 2)) (S (S n))) (H0 (S (S n)))) as [x1 p0]. rewrite applyXabs. + setoid_replace (partialApply (Xminus (Xmult (CharacFunc (fun x2 : X (ElemFunc IS) => forall i : nat, Bi i x2)) (fst x1)) (Xmult (CharacFunc (fun x2 : X (ElemFunc IS) => forall i : nat, Bi i x2)) (fst x0))) x xdf) with (partialApply _ x (fst xdf) - partialApply (XmaxConst (XminConst h (CR_of_Q _ (Z.pos k # 1))) (CR_of_Q _ (Z.neg k # 1))) x (dom x d) + (partialApply (XmaxConst (XminConst h (CR_of_Q _ (Z.pos k # 1))) (CR_of_Q _ (Z.neg k # 1))) x (dom x d) - partialApply (Xmult (CharacFunc (fun x2 : X (ElemFunc IS) => forall i : nat, Bi i x2)) (fst x0)) x (snd xdf))). apply (CRle_trans _ _ _ (CRabs_triang _ _)). rewrite applyXplus, applyXscale, CRmult_0_l, CRplus_0_l. rewrite applyXscale, (CR_of_Q_plus _ 1 1). rewrite CRmult_plus_distr_r, CRmult_plus_distr_r, CRmult_1_l. apply CRplus_le_compat. destruct xdf, d1, d0, d0. simpl. rewrite CRmult_1_r, CRmult_1_l. apply CRlt_asym. destruct p0. specialize (c x (dom x d) d3). apply (CRle_lt_trans _ (CRabs (RealT (ElemFunc IS)) (partialApply (XmaxConst (XminConst h (CR_of_Q (RealT (ElemFunc IS)) (Z.pos k # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg k # 1))) x (dom x d) - partialApply (fst x1) x d3))). rewrite CRabs_minus_sym. apply CRle_refl. apply (CRlt_le_trans _ (eps * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S (S n)))). apply c. exact bSn. simpl. rewrite <- CRmult_assoc. rewrite <- CRmult_assoc. apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. rewrite <- (CRmult_1_r eps), CRmult_assoc, CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite CRmult_1_l, <- CR_of_Q_mult. apply CR_of_Q_le. discriminate. contradiction. destruct xdf, d1, d1. simpl. rewrite CRmult_1_r, CRmult_1_l. apply CRlt_asym. apply (CRlt_le_trans _ (eps * CRpow (CR_of_Q _ (1 # 2)) (S n))). apply (snd p). exact bn. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite <- (CRmult_1_l (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n)). apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. contradiction. unfold CRminus. rewrite CRplus_assoc. destruct xdf. rewrite (applyXminus (Xmult (CharacFunc (fun x2 : X (ElemFunc IS) => forall i : nat, Bi i x2)) (fst x1)) (Xmult (CharacFunc (fun x2 : X (ElemFunc IS) => forall i : nat, Bi i x2)) (fst x0)) x d0 d1). apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. + simpl. rewrite CRmult_0_r, CRmult_0_l. destruct xdf, d0, d0. contradiction. rewrite CRmult_0_l. destruct d1, d0. contradiction. rewrite CRmult_0_l, CRmult_0_r. rewrite CRabs_right. apply CRle_refl. rewrite CRplus_0_r. apply CRle_refl. + rewrite IntegralPlus, IntegralScale, CRmult_0_r, CRplus_0_l. rewrite IntegralScale. rewrite CRmult_comm, <- CRmult_assoc, <- CRmult_assoc. rewrite (CRmult_comm (CR_of_Q (RealT (ElemFunc IS)) 2 * eps)). apply CRle_refl. + apply IntegralNonNeg. intros x xdf. rewrite applyXabs. apply CRabs_pos. - apply series_cv_scale. exact GeoHalfTwo. - destruct lcv. destruct (IntegrableXpointwiseLimit _ fiInt l s) as [limInt fcv]. clear s. refine (IntegrableExtensionalAE _ _ _ _ limInt). + destruct dom as [hdom [hdomInt dom]]. exists (Xplus hdom (XpointwiseLimit (fun i : nat => Xmult (CharacFunc (fun x : X (ElemFunc IS) => forall i0 : nat, Bi i0 x)) (fi i)))). split. apply IntegrablePlus. exact hdomInt. exact limInt. intros x [xdf xdg]. split. 2: exact (dom x xdf). simpl. destruct xdg as [xDn xdg]. destruct (xDn O). exact d. + destruct dom as [hdom [hdomInt dom]]. exists hdom. split. exact hdomInt. intros. unfold sa_approx. apply applyPointwiseLimit. destruct dG, d. simpl in s. apply (CR_cv_proper _ (partialApply (XmaxConst (XminConst h (CR_of_Q (RealT (ElemFunc IS)) (Z.pos k # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg k # 1))) x d0)). 2: simpl; rewrite CRmult_1_l; reflexivity. apply (CR_cv_eq _ (fun n : nat => partialApply (fi n) x (let (xn, _) := dF in snd (xn n)))). intro n. simpl. destruct dF, (x0 n), d. rewrite CRmult_1_l. reflexivity. contradiction. intro p. assert (CR_cv _ (fun i => CRpow (CR_of_Q _ (1 # 2)) i * eps) 0). { apply (CR_cv_proper _ (0 * eps)). apply CR_cv_scale. exact GeoCvZero. apply CRmult_0_l. } specialize (H3 p) as [j jmaj]. exists j. intros. specialize (jmaj j (Nat.le_refl j)). unfold fi. destruct dF. destruct (x0 i). unfold snd. unfold fi in d1. unfold Bi in s. specialize (s i). destruct (H (eps * CRpow (CR_of_Q _ (1 # 2)) (S i)) (H0 (S i))). destruct p0 as [i0 c1]. rewrite CRabs_minus_sym. specialize (c1 x). apply (CRle_trans _ (eps * CRpow (CR_of_Q _ (1 # 2)) (S i))). apply CRlt_asym, c1, s. clear c1. refine (CRle_trans _ _ _ _ jmaj). unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right, CRmult_comm. apply CRmult_le_compat_r. apply CRlt_asym, epsPos. apply Nat.le_exists_sub in H3. destruct H3, H3. subst i. rewrite <- (CRmult_1_l (CRpow (CR_of_Q _ (1 # 2)) j)). replace (S (x2 + j)) with (S x2 + j)%nat. 2: reflexivity. rewrite <- CRpow_plus_distr. apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. apply (CRmult_le_reg_l (CRpow (CR_of_Q _ 2) (S x2))). apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. rewrite CRpow_mult. rewrite <- (CRpow_proper 1). rewrite CRpow_one, CRmult_1_r. apply CRpow_ge_one. apply CR_of_Q_le. discriminate. rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. reflexivity. apply CRmult_le_0_compat. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. apply CRlt_asym, epsPos. unfold sa_approx in n. apply (CR_cv_eq _ (fun _ => 0)). intros. simpl. destruct dF, (x0 n0), d. contradiction. rewrite CRmult_0_l. reflexivity. apply (CR_cv_proper _ 0). apply CR_cv_const. simpl. rewrite CRmult_0_l, CRmin_left, CRmax_left. reflexivity. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile