Proofs of measurable_Rbar_{(g|l)(e|t),(c|o)(c|o)}.

Lebesgue/measurable_Rbar.v

@@ -500,9 +500,9 @@ Proof.
 rewrite measurable_Rbar_eq_Borel; apply measurable_Rbar_Borel_singleton.
 Qed.
 
-Lemma measurable_Rbar_eq_le : measurable_Rbar = measurable gen_Rbar_le.
+Lemma measurable_Rbar_eq_ge : measurable_Rbar = measurable gen_Rbar_ge.
 Proof.
-rewrite <- measurable_Rbar_Borel_eq_le, measurable_Rbar_Borel_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_ge, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_eq_gt : measurable_Rbar = measurable gen_Rbar_gt.
@@ -510,84 +510,56 @@ Proof.
 rewrite <- measurable_Rbar_Borel_eq_gt, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
-Lemma measurable_Rbar_eq_ge : measurable_Rbar = measurable gen_Rbar_ge.
+Lemma measurable_Rbar_eq_le : measurable_Rbar = measurable gen_Rbar_le.
 Proof.
-rewrite <- measurable_Rbar_Borel_eq_ge, measurable_Rbar_Borel_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_le, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
-Lemma measurable_Rbar_lt_R : forall (a : R), measurable_Rbar (Rbar_lt a).
+Lemma measurable_Rbar_ge : forall b, measurable_Rbar (Rbar_ge b).
 Proof.
-intros; apply measurable_gen; easy.
+intros; apply measurable_Rbar_closed, closed_Rbar_ge.
 Qed.
 
-Lemma measurable_Rbar_lt : forall a, measurable_Rbar (Rbar_lt a).
-Proof.
-intros a; destruct a.
-apply measurable_Rbar_lt_R.
-apply measurable_ext with emptyset; try easy; apply measurable_empty.
-apply measurable_ext with (union_seq (fun n => Rbar_lt (- INR n))).
-admit.
-apply measurable_union_seq; intros n; apply measurable_Rbar_lt_R.
-Admitted.
-
-Lemma measurable_Rbar_le_R : forall (a : R), measurable_Rbar (Rbar_le a).
+Lemma measurable_Rbar_gt : forall b, measurable_Rbar (Rbar_gt b).
 Proof.
-intros; rewrite measurable_Rbar_eq_le; apply measurable_gen; easy.
+intros; apply measurable_Rbar_open, open_Rbar_gt.
 Qed.
 
 Lemma measurable_Rbar_le : forall a, measurable_Rbar (Rbar_le a).
 Proof.
-intros a; destruct a.
-apply measurable_Rbar_le_R.
-apply measurable_ext with (singleton p_infty).
-Rbar_interval_full_unfold; intros y; destruct y; easy.
-apply measurable_Rbar_singleton.
-apply measurable_ext with fullset; try easy.
-apply measurable_full.
+intros; apply measurable_Rbar_closed, closed_Rbar_le.
 Qed.
 
-Lemma measurable_Rbar_gt : forall b, measurable_Rbar (Rbar_gt b).
+Lemma measurable_Rbar_lt : forall a, measurable_Rbar (Rbar_lt a).
 Proof.
-intros; apply measurable_compl_rev.
-
-(* We need Rbar_le_not_gt. *)
-
-Admitted.
+intros; apply measurable_Rbar_open, open_Rbar_lt.
+Qed.
 
-Lemma measurable_Rbar_ge : forall b, measurable_Rbar (Rbar_ge b).
+Lemma measurable_Rbar_cc : forall a b, measurable_Rbar (Rbar_cc a b).
 Proof.
-intros; apply measurable_compl_rev.
-
-(* We need Rbar_lt_not_ge. *)
-
-Admitted.
+intros; apply measurable_Rbar_closed, closed_Rbar_intcc.
+Qed.
 
-Lemma measurable_Rbar_oo : forall a b, measurable_Rbar (Rbar_oo a b).
+Lemma measurable_Rbar_co : forall a b, measurable_Rbar (Rbar_co a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_lt.
-apply measurable_Rbar_gt.
+intros; apply measurable_inter;
+    [apply measurable_Rbar_le | apply measurable_Rbar_gt].
 Qed.
 
 Lemma measurable_Rbar_oc : forall a b, measurable_Rbar (Rbar_oc a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_lt.
-apply measurable_Rbar_ge.
+intros; apply measurable_inter;
+    [apply measurable_Rbar_lt | apply measurable_Rbar_ge].
 Qed.
 
-Lemma measurable_Rbar_co : forall a b, measurable_Rbar (Rbar_co a b).
+Lemma measurable_Rbar_oo : forall a b, measurable_Rbar (Rbar_oo a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_le.
-apply measurable_Rbar_gt.
+intros; apply measurable_Rbar_open, open_Rbar_intoo.
 Qed.
 
-Lemma measurable_Rbar_cc : forall a b, measurable_Rbar (Rbar_cc a b).
+Lemma measurable_Rbar_scal :
+  forall B l, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_le.
-apply measurable_Rbar_ge.
-Qed.
+Admitted.
 
 End measurable_Rbar.