proposition: Lemma OpenIntervalIntegrable : forall {R : ConstructiveReals} (a b : CRcarrier R), a < b -> { limInt : @IntegrableSet IntSpaceCSUCFunctions (fun x => CRltProp R a x /\ CRltProp R x b) | MeasureSet limInt == b-a }.
proof: Proof. intros. assert (forall n:nat, 0 < (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) as etaPos. { intro n. apply CRmult_lt_0_compat. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r, H. apply CR_of_Q_pos. reflexivity. } pose (fun n:nat => PartializeFunc (CRcarrier R) (CSUCUnitTrapeze (a + (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) (b - (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) ((b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) (etaPos n))) as fn. assert (forall c d : CRcarrier R, CR_cv R (fun n => c + d * CR_of_Q R (1 # Pos.of_nat (n + 2))) c) as affineCv. { intros. apply (CR_cv_proper _ (c+0) c). apply CR_cv_plus. apply CR_cv_const. apply (CR_cv_proper _ (0*d)). apply (CR_cv_eq _ (fun n : nat => CR_of_Q R (1 # Pos.of_nat (n + 2)) * d)). intro n. apply CRmult_comm. apply CR_cv_scale. intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (Nat.le_trans _ _ _ H0). rewrite Nat.add_comm. apply le_S, le_S, Nat.le_refl. intro abs. rewrite Nat.add_comm in abs. discriminate. apply CR_of_Q_le. discriminate. rewrite CRmult_0_l. reflexivity. rewrite CRplus_0_r. reflexivity. } assert (CR_cv R (fun n => a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) a) as cv_left. { apply affineCv. } assert (CR_cv R (fun n => b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) b) as cv_right. { apply (CR_cv_eq _ (fun n => b + (-(b - a)) * CR_of_Q R (1 # Pos.of_nat (n + 2)))). intro n. apply CRplus_morph. reflexivity. rewrite CRopp_mult_distr_l. reflexivity. apply affineCv. } assert (forall x (xdn : forall n, Domain (fn n) x), (CRltProp R a x /\ CRltProp R x b) -> CR_cv R (fun n => partialApply (fn n) x (xdn n)) 1) as inPlateau. { intros. destruct H0. apply CRltEpsilon in H0. apply CRltEpsilon in H1. destruct (CR_cv_open_above _ x0 a cv_left H0). destruct (CR_cv_open_below _ x0 b cv_right H1). exists (max x1 x2). intros. specialize (c i). specialize (c0 i). simpl. rewrite CSUCTrapezePlateau. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. split; apply CRlt_asym. apply c. apply (Nat.le_trans _ (max x1 x2)). apply Nat.le_max_l. exact H2. apply c0. apply (Nat.le_trans _ (max x1 x2)). apply Nat.le_max_r. exact H2. } assert (forall n:nat, a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2)) <= b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) as fnL. { intro n. apply (CRplus_le_reg_r ((b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2)))). unfold CRminus. rewrite (CRplus_assoc b), CRplus_opp_l, CRplus_0_r. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. rewrite Qinv_plus_distr, CRplus_comm. rewrite <- (CRmult_1_r (-a + b)). rewrite CRmult_assoc. apply CRmult_le_compat_l. rewrite <- (CRplus_opp_l a). apply CRplus_le_compat_l, CRlt_asym, H. rewrite CRmult_1_l. apply CR_of_Q_le. unfold Qle,Qnum,Qden. rewrite Z.mul_1_r, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite Nat.add_comm. apply le_n_S, le_n_S, Nat.le_0_l. intro abs. rewrite Nat.add_comm in abs. discriminate. } assert (PartialRestriction (XpointwiseLimit fn) (CharacFunc (fun x0 : CRcarrier R => CRltProp R a x0 /\ CRltProp R x0 b))). { split. - intros x xdf. simpl. destruct xdf as [xdn c]. apply CR_complete in c. destruct c as [l lcv]. destruct (CRltLinear R). destruct (s 0 l 1 (CRzero_lt_one R)). + left. apply (CR_cv_open_below _ 0) in lcv. 2: exact c. destruct lcv as [n nmaj]. specialize (nmaj n (Nat.le_refl n)). apply (CSUCTrapezeInPlateau (a + (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) (b - (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) ((b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) x (etaPos n)) in nmaj. destruct nmaj. split. apply CRltForget. apply (CRle_lt_trans _ (a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2)) - (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2)))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply CRle_refl. exact c0. unfold CRminus in c1. apply CRltForget. apply (CRlt_le_trans _ _ _ c1). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRle_refl. + right. intro abs. specialize (inPlateau x xdn abs). contradict c. fold (CRle _ 1 l). rewrite (CR_cv_unique _ _ _ inPlateau lcv). apply CRle_refl. - intros. simpl in xG. destruct xG. + apply applyPointwiseLimit. exact (inPlateau _ (fun n => let (xdn,_) := xD in xdn n) a0). + apply applyPointwiseLimit. apply (CR_cv_eq _ (fun _ => 0)). 2: apply CR_cv_const. intros. simpl. unfold CSUCUnitTrapeze, UCUnitHeaviside. rewrite (CRinv_morph _ ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2))) _ (inr (etaPos n0))). rewrite (CRinv_morph (b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)) + (b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)) - (b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))) ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2))) _ (inr (etaPos n0))). destruct (CRltLinear R). destruct (s a x0 b H). assert (b <= x0). { intro abs. apply n. split. apply CRltForget, c. apply CRltForget, abs. } clear c. rewrite CRmin_left, CRmin_left. rewrite CRmax_right. unfold CRminus. rewrite CRplus_opp_r. reflexivity. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. unfold CRminus. rewrite <- CRplus_0_l. rewrite CRopp_plus_distr, CRopp_involutive. do 2 rewrite <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_0_r. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r, H0. apply (CRmult_le_reg_r ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_0_l. rewrite <- CRplus_assoc, <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_0_r, CRplus_0_l. rewrite <- (CRplus_opp_r (a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply CRplus_le_compat_r, (CRle_trans _ b). 2: exact H0. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- (CRmult_1_r (-a+b)), (CRplus_comm (-a)). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. apply CRlt_asym, H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite Nat.add_comm. apply le_n_S, Nat.le_0_l. intro abs. rewrite Nat.add_comm in abs. discriminate. assert (x0 <= a). { intro abs. apply n. split. apply CRltForget, abs. apply CRltForget, c. } clear c. rewrite CRmax_left, CRmax_left. unfold CRminus. rewrite CRplus_opp_r. reflexivity. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. rewrite <- (CRplus_opp_r (b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply CRplus_le_compat_r. apply (CRle_trans _ _ _ H0). apply (CRplus_le_reg_l (-b)). unfold CRminus. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. setoid_replace (-b+a) with (-(b-a)). apply CRopp_ge_le_contravar. rewrite <- (CRmult_1_r (b-a)). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r, CRlt_asym, H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite Nat.add_comm. apply le_n_S, Nat.le_0_l. intro abs. rewrite Nat.add_comm in abs. discriminate. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. reflexivity. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r ((b - a) * CR_of_Q R (1 # Pos.of_nat (n0 + 2)))). apply etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r, H0. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. } destruct (IntegralMonotoneConvergence IntSpaceCSUCFunctions fn (fun n => @IntegrableL IntSpaceCSUCFunctions (fn n) (CSUCTrapeze_IS_CSUC (a + (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) (b - (b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) ((b-a) * CR_of_Q R (1#Pos.of_nat (n+2))) (etaPos n) (fnL n))) (b-a)) as [limInt mesRect]. - intros n x xdf xdg. unfold fn, PartializeFunc, partialApply. apply TrapezeIncluded. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. apply CRmult_le_compat_l. apply CRle_minus, CRlt_asym, H. apply CR_of_Q_le. unfold Qle,Qnum,Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. apply le_S, Nat.le_refl. discriminate. intro abs. rewrite Nat.add_comm in abs. discriminate. - simpl. apply (CR_cv_eq _ (fun n => b-a + (-(b-a)) * CR_of_Q R (1 # Pos.of_nat (n + 2)))). 2: apply affineCv. intro n. rewrite IntegralLstable. simpl. symmetry. unfold fn. unfold IntegralCSUC, CSUCTrapeze_IS_CSUC, CSUC_fullDomain, CSUC_low; simpl. rewrite (UC_integral_extens _ (CSUCUnitTrapeze (a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) (b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) ((b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) (etaPos n)) _ _ _ (fun eps epsPos => eps * CR_of_Q R (1#2) * ((b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2)))) _ (CSUCUnitTrapeze_cont _ _ _ _ (fnL n)) _ (TrapezeLe _ _ _ (etaPos n) (fnL n))). 2: intros; reflexivity. rewrite (CSUCUnitTrapezeInt (a + (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) (b - (b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) ((b - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))) (etaPos n) (fnL n)). unfold CRminus. rewrite CRplus_comm, CRopp_plus_distr, CRplus_assoc. rewrite <- (CRplus_assoc (- ((b + - a) * CR_of_Q R (1 # Pos.of_nat (n + 2))))). rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, (CRplus_comm (-a)). rewrite CRopp_mult_distr_l. reflexivity. - exists (@IntegrableFunctionExtensional IntSpaceCSUCFunctions _ _ X limInt). unfold MeasureSet. rewrite IntegralRestrict. exact mesRect. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets