Add some results + cleaning.

WIP: being lazy with proofs of measurable_Rbar_abs and measurable_Rbar_scal.

Lebesgue/UniformSpace_compl.v

@@ -542,6 +542,13 @@ apply Rlt_le_trans with (k * f); try apply Rmult_lt_compat_l; try easy.
 apply Rabs_lt_between'; easy.
 Qed.
 
+Lemma open_Rbar_is_finite : open is_finite.
+Proof.
+pose (full := fun _ : R => True).
+apply open_ext with (fun y => is_finite y /\ full y); try (unfold full; tauto).
+apply open_R_Rbar, open_true.
+Qed.
+
 Lemma open_Rbar_R : forall B, open B -> open (fun x => B (Finite x)).
 Proof.
 intros B HB x Hx.

Lebesgue/measurable_Rbar.v

@@ -63,36 +63,6 @@ Proof.
 intros; apply measurable_Borel_closed, closed_Rbar_eq.
 Qed.
 
-(*
-Lemma measurable_Rbar_Borel_ge : forall b, measurable_Rbar_Borel (Rbar_ge b).
-Proof.
-intros; apply measurable_Borel_closed, closed_Rbar_ge.
-Qed.
-
-Lemma measurable_Rbar_Borel_gt : forall b, measurable_Rbar_Borel (Rbar_gt b).
-Proof.
-intros; apply measurable_Borel_open, open_Rbar_gt.
-Qed.
-
-Lemma measurable_Rbar_Borel_le : forall a, measurable_Rbar_Borel (Rbar_le a).
-Proof.
-intros; apply measurable_Borel_closed, closed_Rbar_le.
-Qed.
-
-Lemma measurable_Rbar_Borel_lt : forall a, measurable_Rbar_Borel (Rbar_lt a).
-Proof.
-intros; apply measurable_Borel_open, open_Rbar_lt.
-Qed.
-
-Lemma measurable_Rbar_Borel_oo :
-  forall a b, measurable_Rbar_Borel (Rbar_oo a b).
-Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_Borel_lt.
-apply measurable_Rbar_Borel_gt.
-Qed.
-*)
-
 Lemma measurable_Rbar_Borel_up_id :
   forall A, measurable_R A -> measurable_Rbar_Borel (up_id A).
 Proof.
@@ -557,6 +527,26 @@ Proof.
 intros; apply measurable_Rbar_open, open_Rbar_intoo.
 Qed.
 
+Lemma measurable_Rbar_is_finite : measurable_Rbar is_finite.
+Proof.
+apply measurable_Rbar_open, open_Rbar_is_finite.
+Qed.
+
+Lemma measurable_Rbar_eq_R : measurable_Rbar = measurable_Rbar_R.
+Proof.
+rewrite measurable_Rbar_eq_Borel, measurable_Rbar_R_correct; easy.
+Qed.
+
+Lemma measurable_Rbar_eq_R_alt : measurable_Rbar = measurable_Rbar_R_alt.
+Proof.
+rewrite measurable_Rbar_eq_Borel, measurable_Rbar_R_alt_correct; easy.
+Qed.
+
+Lemma measurable_Rbar_abs :
+  forall B, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_abs y)).
+Proof.
+Admitted.
+
 Lemma measurable_Rbar_scal :
   forall B l, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
 Proof.