Renaming (unique prefix = measurable_Rbar_).

Lebesgue/measurable_Rbar.v

@@ -37,57 +37,100 @@ Section measurable_Rbar_Borel_Def.
     + the union of Borel subsets of R, -infty, and infty.
  *)
 
-Definition measurable_Borel_Rbar : (Rbar -> Prop) -> Prop :=
+Definition measurable_Rbar_Borel : (Rbar -> Prop) -> Prop :=
   @measurable_Borel Rbar_UniformSpace.
 
 Definition measurable_Rbar_R : (Rbar -> Prop) -> Prop :=
   fun B => measurable_R (down B).
 
-Inductive measurable_R_Rbar : (Rbar -> Prop) -> Prop :=
-  | MRRb : forall A, measurable_R A -> measurable_R_Rbar (up_id A)
-  | MRRb_m : forall A, measurable_R A -> measurable_R_Rbar (up_m A)
-  | MRRb_p : forall A, measurable_R A -> measurable_R_Rbar (up_p A)
-  | MRRb_mp : forall A, measurable_R A -> measurable_R_Rbar (up_mp A).
+Inductive measurable_Rbar_R_alt : (Rbar -> Prop) -> Prop :=
+  | MRRb : forall A, measurable_R A -> measurable_Rbar_R_alt (up_id A)
+  | MRRb_m : forall A, measurable_R A -> measurable_Rbar_R_alt (up_m A)
+  | MRRb_p : forall A, measurable_R A -> measurable_Rbar_R_alt (up_p A)
+  | MRRb_mp : forall A, measurable_R A -> measurable_Rbar_R_alt (up_mp A).
 
 End measurable_Rbar_Borel_Def.
 
 
 Section measurable_Rbar_Borel_Facts.
 
-(** Preliminary results on measurable_Borel_Rbar. *)
+(** Preliminary results on measurable_Rbar_Borel. *)
 
-Lemma measurable_Borel_Rbar_ge : forall b, measurable_Borel_Rbar (Rbar_ge b).
+Lemma measurable_Rbar_Borel_singleton :
+  forall a, measurable_Rbar_Borel (singleton a).
+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_Borel_Rbar_gt : forall b, measurable_Borel_Rbar (Rbar_gt b).
+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_Borel_Rbar_le : forall a, measurable_Borel_Rbar (Rbar_le a).
+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_Borel_Rbar_lt : forall a, measurable_Borel_Rbar (Rbar_lt a).
+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_Borel_Rbar_singleton :
-  forall a, measurable_Borel_Rbar (singleton a).
+Lemma measurable_Rbar_Borel_oo :
+  forall a b, measurable_Rbar_Borel (Rbar_oo a b).
 Proof.
-intros; apply measurable_Borel_closed, closed_Rbar_eq.
+intros; apply measurable_inter.
+apply measurable_Rbar_Borel_lt.
+apply measurable_Rbar_Borel_gt.
 Qed.
+*)
 
-Lemma measurable_Borel_Rbar_oo :
-  forall a b, measurable_Borel_Rbar (Rbar_oo a b).
+Lemma measurable_Rbar_Borel_up_id :
+  forall A, measurable_R A -> measurable_Rbar_Borel (up_id A).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Borel_Rbar_lt.
-apply measurable_Borel_Rbar_gt.
+rewrite measurable_R_eq_Borel.
+intros A HA; induction HA as [A HA | | A HA1 HA2 | A HA1 HA2].
+(* *)
+apply measurable_gen; rewrite <- Rbar_subset_open_correct; apply RbSO_woinf; easy.
+(* *)
+apply measurable_ext with emptyset;
+    [rewrite <- up_id_empty at 1; easy | apply measurable_empty].
+(* *)
+rewrite up_id_compl; apply measurable_compl.
+repeat apply measurable_union; try easy; apply measurable_Rbar_Borel_singleton.
+(* *)
+rewrite up_id_union_seq; apply measurable_union_seq; easy.
+Qed.
+
+Lemma measurable_Rbar_Borel_up_m :
+  forall A, measurable_R A -> measurable_Rbar_Borel (up_m A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Rbar_Borel_up_id; easy.
+apply measurable_Rbar_Borel_singleton.
+Qed.
+
+Lemma measurable_Rbar_Borel_up_p :
+  forall A, measurable_R A -> measurable_Rbar_Borel (up_p A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Rbar_Borel_up_id; easy.
+apply measurable_Rbar_Borel_singleton.
+Qed.
+
+Lemma measurable_Rbar_Borel_up_mp :
+  forall A, measurable_R A -> measurable_Rbar_Borel (up_mp A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Rbar_Borel_up_m; easy.
+apply measurable_Rbar_Borel_singleton.
 Qed.
 
 (** Preliminary results on measurable_Rbar_R. *)
@@ -132,76 +175,18 @@ induction HB as [A B HA HB | A a b HA]; [induction HB as [b Hb | a Ha] | ];
 all: try apply measurable_Rbar_R_gt; apply measurable_Rbar_R_lt.
 Qed.
 
-Lemma measurable_Rbar_R_empty : wEmpty measurable_Rbar_R.
+Lemma measurable_Rbar_R_is_sigma_algebra : is_Sigma_algebra measurable_Rbar_R.
 Proof.
-unfold measurable_Rbar_R, wEmpty.
+apply Sigma_algebra_equiv; repeat split; unfold measurable_Rbar_R, wEmpty.
 rewrite down_empty; apply measurable_empty.
-Qed.
-
-Lemma measurable_Rbar_R_compl : Compl measurable_Rbar_R.
-Proof.
-unfold measurable_Rbar_R.
 intros A; rewrite down_compl; apply measurable_compl; easy.
-Qed.
-
-Lemma measurable_Rbar_R_union_seq : Union_seq measurable_Rbar_R.
-Proof.
-unfold measurable_Rbar_R.
 intros A HA; rewrite down_union_seq; apply measurable_union_seq; easy.
 Qed.
 
-Lemma measurable_Rbar_R_is_sigma_algebra : is_Sigma_algebra measurable_Rbar_R.
-Proof.
-apply Sigma_algebra_equiv; repeat split.
-apply measurable_Rbar_R_empty.
-apply measurable_Rbar_R_compl.
-apply measurable_Rbar_R_union_seq.
-Qed.
-
-Lemma measurable_Borel_Rbar_R_up_id :
-  forall A, measurable_R A -> measurable_Borel_Rbar (up_id A).
-Proof.
-rewrite measurable_R_eq_Borel.
-intros A HA; induction HA as [A HA | | A HA1 HA2 | A HA1 HA2].
-(* *)
-apply measurable_gen; rewrite <- Rbar_subset_open_correct; apply RbSO_woinf; easy.
-(* *)
-apply measurable_ext with emptyset;
-    [rewrite <- up_id_empty at 1; easy | apply measurable_empty].
-(* *)
-rewrite up_id_compl; apply measurable_compl.
-repeat apply measurable_union; try easy; apply measurable_Borel_Rbar_singleton.
-(* *)
-rewrite up_id_union_seq; apply measurable_union_seq; easy.
-Qed.
-
-Lemma measurable_Borel_Rbar_R_up_m :
-  forall A, measurable_R A -> measurable_Borel_Rbar (up_m A).
-Proof.
-intros; apply measurable_union.
-apply measurable_Borel_Rbar_R_up_id; easy.
-apply measurable_Borel_Rbar_singleton.
-Qed.
-
-Lemma measurable_Borel_Rbar_R_up_p :
-  forall A, measurable_R A -> measurable_Borel_Rbar (up_p A).
-Proof.
-intros; apply measurable_union.
-apply measurable_Borel_Rbar_R_up_id; easy.
-apply measurable_Borel_Rbar_singleton.
-Qed.
-
-Lemma measurable_Borel_Rbar_R_up_mp :
-  forall A, measurable_R A -> measurable_Borel_Rbar (up_mp A).
-Proof.
-intros; apply measurable_union.
-apply measurable_Borel_Rbar_R_up_m; easy.
-apply measurable_Borel_Rbar_singleton.
-Qed.
-
 (** Correctness results. *)
 
-Lemma measurable_Rbar_R_eq : measurable_Rbar_R = measurable_R_Rbar.
+Lemma measurable_Rbar_R_eq :
+  measurable_Rbar_R = measurable_Rbar_R_alt.
 Proof.
 apply Ext_equiv; split; intros B; unfold measurable_Rbar_R.
 (* *)
@@ -218,30 +203,34 @@ rewrite down_up_p; easy.
 rewrite down_up_mp; easy.
 Qed.
 
-Lemma measurable_Rbar_R_Borel : Incl measurable_Borel_Rbar measurable_Rbar_R.
+Lemma measurable_Rbar_Borel_R :
+  Incl measurable_Rbar_Borel measurable_Rbar_R.
 Proof.
 apply measurable_gen_lub_alt.
 apply measurable_Rbar_R_is_sigma_algebra.
 apply measurable_Rbar_R_open.
 Qed.
 
-Lemma measurable_Borel_Rbar_R : Incl measurable_R_Rbar measurable_Borel_Rbar.
+Lemma measurable_Rbar_R_alt_Borel :
+  Incl measurable_Rbar_R_alt measurable_Rbar_Borel.
 Proof.
 intros B HB; induction HB as [A HA | A HA | A HA | A HA].
-apply measurable_Borel_Rbar_R_up_id; easy.
-apply measurable_Borel_Rbar_R_up_m; easy.
-apply measurable_Borel_Rbar_R_up_p; easy.
-apply measurable_Borel_Rbar_R_up_mp; easy.
+apply measurable_Rbar_Borel_up_id; easy.
+apply measurable_Rbar_Borel_up_m; easy.
+apply measurable_Rbar_Borel_up_p; easy.
+apply measurable_Rbar_Borel_up_mp; easy.
 Qed.
 
-Lemma measurable_Rbar_R_correct : measurable_Rbar_R = measurable_Borel_Rbar.
+Lemma measurable_Rbar_R_correct :
+  measurable_Rbar_R = measurable_Rbar_Borel.
 Proof.
 apply Ext_equiv; split.
-rewrite measurable_Rbar_R_eq; apply measurable_Borel_Rbar_R.
-apply measurable_Rbar_R_Borel.
+rewrite measurable_Rbar_R_eq; apply measurable_Rbar_R_alt_Borel.
+apply measurable_Rbar_Borel_R.
 Qed.
 
-Lemma measurable_R_Rbar_correct : measurable_R_Rbar = measurable_Borel_Rbar.
+Lemma measurable_Rbar_R_alt_correct :
+  measurable_Rbar_R_alt = measurable_Rbar_Borel.
 Proof.
 rewrite <- measurable_Rbar_R_eq; apply measurable_Rbar_R_correct.
 Qed.
@@ -375,7 +364,7 @@ Admitted.
 End gen_Rbar_Facts2.
 
 
-Section measurable_Borel_Rbar_eq.
+Section measurable_Rbar_Borel_eq.
 
 Lemma measurable_Rbar_lt_Rbar_R :
   Incl measurable_Rbar_R (measurable gen_Rbar_lt).
@@ -388,8 +377,8 @@ induction HA as [B [a]]; easy.
 induction HA as [a]; rewrite (subset_ext _ (down (Rbar_lt a))); easy.
 Qed.
 
-Lemma measurable_Rbar_lt_R_Rbar :
-  Incl measurable_R_Rbar (measurable gen_Rbar_lt).
+Lemma measurable_Rbar_lt_Rbar_R_alt :
+  Incl measurable_Rbar_R_alt (measurable gen_Rbar_lt).
 Proof.
 intros B HB; induction HB as [A HA | A HA | A HA | A HA];
     rewrite measurable_R_eq_lt in HA.
@@ -406,11 +395,11 @@ apply measurable_ext with (Rlt a); try easy.
 apply measurable_R_lt.
 Qed.
 
-Lemma measurable_Borel_Rbar_eq_lt :
-  measurable_Borel_Rbar = measurable gen_Rbar_lt.
+Lemma measurable_Rbar_Borel_eq_lt :
+  measurable_Rbar_Borel = measurable gen_Rbar_lt.
 Proof.
 apply Ext_equiv; split.
-rewrite <- measurable_R_Rbar_correct; apply measurable_Rbar_lt_R_Rbar.
+rewrite <- measurable_Rbar_R_alt_correct; apply measurable_Rbar_lt_Rbar_R_alt.
 rewrite <- measurable_Rbar_R_correct; apply measurable_Rbar_R_lt_alt.
 Qed.
 
@@ -424,8 +413,8 @@ destruct (Nat.Even_Odd_False _ Hn); exists n; easy.
 rewrite Rbar_oo_diag_is_empty; easy.
 Qed.
 
-Lemma measurable_Borel_Rbar_eq_topo_basis :
-  measurable_Borel_Rbar = measurable gen_Rbar_topo_basis.
+Lemma measurable_Rbar_Borel_eq_topo_basis :
+  measurable_Rbar_Borel = measurable gen_Rbar_topo_basis.
 Proof.
 apply measurable_Borel_gen_ext; intros B HB.
 (* *)
@@ -449,10 +438,10 @@ Lemma measurable_Rbar_lt_gt :
 Proof.
 Admitted.
 
-Lemma measurable_Borel_Rbar_eq_lt' :
-  measurable_Borel_Rbar = measurable gen_Rbar_lt.
+Lemma measurable_Rbar_Borel_eq_lt' :
+  measurable_Rbar_Borel = measurable gen_Rbar_lt.
 Proof.
-rewrite measurable_Borel_Rbar_eq_topo_basis.
+rewrite measurable_Rbar_Borel_eq_topo_basis.
 apply measurable_gen_ext; intros B HB.
 (* *)
 induction HB as [n]; unfold topo_basis_Rbar.
@@ -466,22 +455,22 @@ apply measurable_gen.
 
 Admitted.
 
-Lemma measurable_Borel_Rbar_eq_le :
-  measurable_Borel_Rbar = measurable gen_Rbar_le.
+Lemma measurable_Rbar_Borel_eq_le :
+  measurable_Rbar_Borel = measurable gen_Rbar_le.
 Proof.
 Admitted.
 
-Lemma measurable_Borel_Rbar_eq_gt :
-  measurable_Borel_Rbar = measurable gen_Rbar_gt.
+Lemma measurable_Rbar_Borel_eq_gt :
+  measurable_Rbar_Borel = measurable gen_Rbar_gt.
 Proof.
 Admitted.
 
-Lemma measurable_Borel_Rbar_eq_ge :
-  measurable_Borel_Rbar = measurable gen_Rbar_ge.
+Lemma measurable_Rbar_Borel_eq_ge :
+  measurable_Rbar_Borel = measurable gen_Rbar_ge.
 Proof.
 Admitted.
 
-End measurable_Borel_Rbar_eq.
+End measurable_Rbar_Borel_eq.
 
 
 Section measurable_Rbar.
@@ -491,7 +480,7 @@ Definition measurable_Rbar := measurable gen_Rbar.
 
 Lemma measurable_Rbar_eq_Borel : measurable_Rbar = measurable_Borel.
 Proof.
-unfold measurable_Rbar, gen_Rbar; rewrite <- measurable_Borel_Rbar_eq_lt; easy.
+unfold measurable_Rbar, gen_Rbar; rewrite <- measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_open : Incl open measurable_Rbar.
@@ -506,22 +495,22 @@ Qed.
 
 Lemma measurable_Rbar_singleton : forall a, measurable_Rbar (singleton a).
 Proof.
-rewrite measurable_Rbar_eq_Borel; apply measurable_Borel_Rbar_singleton.
+rewrite measurable_Rbar_eq_Borel; apply measurable_Rbar_Borel_singleton.
 Qed.
 
 Lemma measurable_Rbar_eq_le : measurable_Rbar = measurable gen_Rbar_le.
 Proof.
-rewrite <- measurable_Borel_Rbar_eq_le, measurable_Borel_Rbar_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_le, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_eq_gt : measurable_Rbar = measurable gen_Rbar_gt.
 Proof.
-rewrite <- measurable_Borel_Rbar_eq_gt, measurable_Borel_Rbar_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_gt, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_eq_ge : measurable_Rbar = measurable gen_Rbar_ge.
 Proof.
-rewrite <- measurable_Borel_Rbar_eq_ge, measurable_Borel_Rbar_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_ge, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_lt_R : forall (a : R), measurable_Rbar (Rbar_lt a).