WIP: proofs of measurable_Borel_Rbar_eq_(l|g)(t|e).

Proofs of measurable_Rbar_*.

Lebesgue/measurable_Rbar.v

@@ -14,19 +14,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import (*Qreals*) Reals Lra.
-From Coquelicot Require Import Coquelicot.
+From Coq Require Import Qreals Reals Lra.
+From Coquelicot Require Import Hierarchy Rbar.
 
-(*Require Import countable_sets.*)
-(*Require Import topo_bases_R.*)
-(*Require Import R_compl.*)
-Require Import Rbar_compl.
-Require Import UniformSpace_compl.
-
-Require Import Subset Subset_seq Subset_R Subset_Rbar.
-Require Import Subset_system_base Subset_system measurable measurable_R.
-
-Open Scope R_scope.
+Require Import nat_compl countable_sets R_compl Rbar_compl UniformSpace_compl.
+Require Import Subset Subset_dec Subset_seq Subset_R Subset_Rbar.
+Require Import Subset_system_base Subset_system.
+Require Import measurable measurable_R.
 
 
 Section measurable_Rbar_Borel_Def.
@@ -60,7 +54,7 @@ End measurable_Rbar_Borel_Def.
 
 Section measurable_Rbar_Borel_Facts.
 
-(** Preliminary results. *)
+(** Preliminary results on measurable_Borel_Rbar. *)
 
 Lemma measurable_Borel_Rbar_ge : forall b, measurable_Borel_Rbar (Rbar_ge b).
 Proof.
@@ -88,25 +82,16 @@ Proof.
 intros; apply measurable_Borel_closed, closed_Rbar_eq.
 Qed.
 
-(** Correctness results. *)
-
-Lemma measurable_Rbar_R_eq : measurable_Rbar_R = measurable_R_Rbar.
+Lemma measurable_Borel_Rbar_oo :
+  forall a b, measurable_Borel_Rbar (Rbar_oo a b).
 Proof.
-apply Ext_equiv; split; intros B; unfold measurable_Rbar_R.
-(* *)
-generalize (Rbar_subset_correct B); intros HB; induction HB.
-rewrite down_up_id; apply MRRb; easy.
-rewrite down_up_m; apply MRRb_m; easy.
-rewrite down_up_p; apply MRRb_p; easy.
-rewrite down_up_mp; apply MRRb_mp; easy.
-(* *)
-intros HB; induction HB.
-rewrite down_up_id; easy.
-rewrite down_up_m; easy.
-rewrite down_up_p; easy.
-rewrite down_up_mp; easy.
+intros; apply measurable_inter.
+apply measurable_Borel_Rbar_lt.
+apply measurable_Borel_Rbar_gt.
 Qed.
 
+(** Preliminary results on measurable_Rbar_R. *)
+
 Lemma measurable_Rbar_R_open_R :
   Incl open (fun A => measurable_Rbar_R (up_id A)).
 Proof.
@@ -120,8 +105,7 @@ unfold measurable_Rbar_R.
 intros A B HA; rewrite down_union; apply measurable_union; easy.
 Qed.
 
-Lemma measurable_Rbar_R_gt :
-  forall a, measurable_Rbar_R (Rbar_gt a).
+Lemma measurable_Rbar_R_gt : forall a, measurable_Rbar_R (Rbar_gt a).
 Proof.
 unfold measurable_Rbar_R; intros a; destruct a.
 rewrite Rbar_gt_eq, down_up_m; apply measurable_R_gt.
@@ -129,8 +113,7 @@ rewrite Rbar_gt_p_eq, down_up_m; apply measurable_full.
 apply measurable_ext with emptyset; [Rbar_interval_auto | apply measurable_empty].
 Qed.
 
-Lemma measurable_Rbar_R_lt :
-  forall a, measurable_Rbar_R (Rbar_lt a).
+Lemma measurable_Rbar_R_lt : forall a, measurable_Rbar_R (Rbar_lt a).
 Proof.
 unfold measurable_Rbar_R; intros a; destruct a.
 rewrite Rbar_lt_eq, down_up_p; apply measurable_R_lt.
@@ -175,13 +158,6 @@ apply measurable_Rbar_R_compl.
 apply measurable_Rbar_R_union_seq.
 Qed.
 
-Lemma measurable_Rbar_R_Borel : Incl measurable_Borel_Rbar 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_up_id :
   forall A, measurable_R A -> measurable_Borel_Rbar (up_id A).
 Proof.
@@ -223,6 +199,32 @@ 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.
+Proof.
+apply Ext_equiv; split; intros B; unfold measurable_Rbar_R.
+(* *)
+generalize (Rbar_subset_correct B); intros HB; induction HB.
+rewrite down_up_id; apply MRRb; easy.
+rewrite down_up_m; apply MRRb_m; easy.
+rewrite down_up_p; apply MRRb_p; easy.
+rewrite down_up_mp; apply MRRb_mp; easy.
+(* *)
+intros HB; induction HB.
+rewrite down_up_id; easy.
+rewrite down_up_m; easy.
+rewrite down_up_p; easy.
+rewrite down_up_mp; easy.
+Qed.
+
+Lemma measurable_Rbar_R_Borel : Incl measurable_Borel_Rbar 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.
 Proof.
 intros B HB; induction HB as [A HA | A HA | A HA | A HA].
@@ -250,59 +252,307 @@ End measurable_Rbar_Borel_Facts.
 Section gen_Rbar_Def.
 
 Inductive gen_Rbar_ge : (Rbar -> Prop) -> Prop :=
-  Gen_Rbar_ge : forall (b : R), gen_Rbar_ge (Rbar_ge b).
+  GRb_ge : forall (b : R), gen_Rbar_ge (Rbar_ge b).
 Inductive gen_Rbar_gt : (Rbar -> Prop) -> Prop :=
-  Gen_Rbar_gt : forall (b : R), gen_Rbar_gt (Rbar_gt b).
+  GRb_gt : forall (b : R), gen_Rbar_gt (Rbar_gt b).
 Inductive gen_Rbar_le : (Rbar -> Prop) -> Prop :=
-  Gen_Rbar_le : forall (a : R), gen_Rbar_le (Rbar_le a).
+  GRb_le : forall (a : R), gen_Rbar_le (Rbar_le a).
 Inductive gen_Rbar_lt : (Rbar -> Prop) -> Prop :=
-  Gen_Rbar_lt : forall (a : R), gen_Rbar_lt (Rbar_lt a).
+  GRb_lt : forall (a : R), gen_Rbar_lt (Rbar_lt a).
+
+Inductive gen_Rbar_topo_basis : (Rbar -> Prop) -> Prop :=
+  GRb_tb : forall n, gen_Rbar_topo_basis (topo_basis_Rbar n).
 
 End gen_Rbar_Def.
 
 
-Section measurable_Rbar.
+Section gen_Rbar_Facts1.
+
+Variable G : (R -> Prop) -> Prop.
+
+Inductive Up_id_G : (Rbar -> Prop) -> Prop :=
+  UG_id : forall A, G A -> Up_id_G (up_id A).
+
+Hypothesis measurable_Up_id_G_singleton :
+  forall y, measurable Up_id_G (singleton y).
+
+Lemma measurable_Rbar_gen_lub_up_id :
+  Incl (measurable G) (fun A => measurable Up_id_G (up_id A)).
+Proof.
+intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
+apply measurable_gen; easy.
+rewrite up_id_empty; apply measurable_empty.
+rewrite up_id_compl; apply measurable_compl.
+repeat apply measurable_union; easy.
+rewrite up_id_union_seq; apply measurable_union_seq; easy.
+Qed.
+
+Inductive Up_mp_G : (Rbar -> Prop) -> Prop :=
+  UG_mp : forall A, G A -> Up_mp_G (up_mp A).
+
+Hypothesis measurable_Up_mp_G_singleton :
+  forall y, measurable Up_mp_G (singleton y).
+
+Lemma measurable_Rbar_gen_lub_up_mp :
+  Incl (measurable G) (fun A => measurable Up_mp_G (up_mp A)).
+Proof.
+intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
+apply measurable_gen; easy.
+repeat apply measurable_union; try easy.
+rewrite up_id_empty; apply measurable_empty.
+rewrite up_mp_compl; apply measurable_compl.
+apply measurable_ext with (diff (up_mp A) (pair m_infty p_infty)).
+Rbar_subset_full_unfold; intros y; destruct y; simpl; repeat split;
+    intros; try easy; try tauto; intros Hy; destruct Hy; easy.
+apply measurable_diff; try easy.
+apply measurable_union; easy.
+rewrite up_mp_union_seq; apply measurable_union_seq; easy.
+Qed.
+
+End gen_Rbar_Facts1.
+
+
+Section gen_Rbar_Facts2.
+
+Variable Gbar : (Rbar -> Prop) -> Prop.
+
+Inductive Down_Gbar : (R -> Prop) -> Prop :=
+  DGb : forall B, Gbar B -> Down_Gbar (down B).
+
+Lemma measurable_Rbar_gen_lub_down :
+  Incl (fun B => measurable Down_Gbar (down B)) (measurable Gbar).
+Proof.
+intros B HB.
+destruct (in_dec B m_infty) as [Hm | Hm], (in_dec B p_infty) as [Hp | Hp].
+rewrite <- up_mp_down; try easy.
+
+Admitted.
+
+End gen_Rbar_Facts2.
+
+
+Section measurable_Borel_Rbar_eq.
+
+Lemma measurable_Rbar_lt_Rbar_R :
+  Incl measurable_Rbar_R (measurable gen_Rbar_lt).
+Proof.
+intros B HB; unfold measurable_Rbar_R in HB; rewrite measurable_R_eq_lt in HB.
+apply measurable_Rbar_gen_lub_down.
+rewrite (Ext (Down_Gbar gen_Rbar_lt) gen_R_lt); try easy.
+clear B HB; intros A; split; intros HA.
+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).
+Proof.
+intros B HB; induction HB as [A HA | A HA | A HA | A HA];
+    rewrite measurable_R_eq_lt in HA.
+
+Admitted.
 
-Lemma measurable_Rbar_R_eq_lt :
+Lemma measurable_Rbar_R_lt_alt :
+  Incl (measurable gen_Rbar_lt) measurable_Rbar_R.
+Proof.
+apply measurable_gen_lub_alt.
+apply measurable_Rbar_R_is_sigma_algebra.
+intros B HB; induction HB as [a].
+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.
 Proof.
-rewrite <- measurable_Rbar_R_correct.
-apply Ext_equiv; split; intros B HB.
+apply Ext_equiv; split.
+rewrite <- measurable_R_Rbar_correct; apply measurable_Rbar_lt_R_Rbar.
+rewrite <- measurable_Rbar_R_correct; apply measurable_Rbar_R_lt_alt.
+Qed.
+
+Lemma gen_Rbar_topo_basis_empty : gen_Rbar_topo_basis emptyset.
+Proof.
+pose (n := bij_Q2N (0, 0)%Q).
+rewrite subset_ext with (B := topo_basis_Rbar (2 * n + 1)%nat); try easy.
+unfold topo_basis_Rbar.
+destruct (Even_Odd_dec (2 * n + 1)%nat) as [Hn | Hn].
+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.
+Proof.
+apply measurable_Borel_gen_ext; intros B HB.
 (* *)
-unfold measurable_Rbar_R in HB.
-admit.
+induction HB as [n]; unfold topo_basis_Rbar.
+destruct (Even_Odd_dec n).
+destruct (Even_Odd_dec (Nat.div2 n)).
+apply open_Rbar_lt.
+apply open_Rbar_gt.
+apply open_Rbar_intoo.
+(* *)
+destruct (Rbar_second_countable_alt B HB) as [P HP].
+exists (fun n => inter (Prop_cst (P n)) (topo_basis_Rbar n)); split; try easy.
+subset_unfold; intros n; case (in_dec P n); intros Hn.
+rewrite subset_ext with (B := topo_basis_Rbar n); easy.
+rewrite subset_ext with (B := emptyset); try easy.
+apply gen_Rbar_topo_basis_empty.
+Qed.
 
+Lemma measurable_Rbar_lt_gt :
+  forall b, b <> m_infty -> measurable gen_Rbar_lt (Rbar_gt b).
+Proof.
+Admitted.
 
+Lemma measurable_Borel_Rbar_eq_lt' :
+  measurable_Borel_Rbar = measurable gen_Rbar_lt.
+Proof.
+rewrite measurable_Borel_Rbar_eq_topo_basis.
+apply measurable_gen_ext; intros B HB.
 (* *)
-induction HB as [B HB | | B HB1 HB2 | B HB1 HB2].
-induction HB; apply measurable_Rbar_R_lt.
-apply measurable_Rbar_R_empty.
-apply measurable_Rbar_R_compl; easy.
-apply measurable_Rbar_R_union_seq; easy.
+induction HB as [n]; unfold topo_basis_Rbar.
+destruct (Even_Odd_dec n) as [Hn1 | Hn1]; try apply measurable_inter.
+destruct (Even_Odd_dec (Nat.div2 n)) as [Hn2 | Hn2].
+1,3: apply measurable_gen; easy.
+1,2: apply measurable_Rbar_lt_gt; easy.
+(* *)
+induction HB as [a].
+apply measurable_gen.
+
 Admitted.
 
-Lemma measurable_Rbar_R_eq_gt :
-  measurable_Borel_Rbar = measurable gen_Rbar_gt.
+Lemma measurable_Borel_Rbar_eq_le :
+  measurable_Borel_Rbar = measurable gen_Rbar_le.
 Proof.
-rewrite measurable_Rbar_R_eq_lt.
-apply measurable_gen_ext; intros A HA; induction HA.
 Admitted.
 
-Lemma measurable_Rbar_ge_singleton :
-  forall y, measurable gen_Rbar_ge (singleton y).
+Lemma measurable_Borel_Rbar_eq_gt :
+  measurable_Borel_Rbar = measurable gen_Rbar_gt.
 Proof.
 Admitted.
 
-Lemma measurable_Rbar_R_eq_ge :
+Lemma measurable_Borel_Rbar_eq_ge :
   measurable_Borel_Rbar = measurable gen_Rbar_ge.
 Proof.
-apply Ext_equiv; split; intros B HB.
-(* *)
-rewrite <- measurable_Rbar_R_correct in HB.
-
 Admitted.
 
-Definition gen_Rbar := gen_Rbar_ge.
+End measurable_Borel_Rbar_eq.
+
+
+Section measurable_Rbar.
+
+Definition gen_Rbar := gen_Rbar_lt.
 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.
+Qed.
+
+Lemma measurable_Rbar_open : Incl open measurable_Rbar.
+Proof.
+rewrite measurable_Rbar_eq_Borel; apply measurable_Borel_open.
+Qed.
+
+Lemma measurable_Rbar_closed : Incl closed measurable_Rbar.
+Proof.
+rewrite measurable_Rbar_eq_Borel; apply measurable_Borel_closed.
+Qed.
+
+Lemma measurable_Rbar_singleton : forall a, measurable_Rbar (singleton a).
+Proof.
+rewrite measurable_Rbar_eq_Borel; apply measurable_Borel_Rbar_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.
+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.
+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.
+Qed.
+
+Lemma measurable_Rbar_lt_R : forall (a : R), measurable_Rbar (Rbar_lt a).
+Proof.
+intros; apply measurable_gen; easy.
+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).
+Proof.
+intros; rewrite measurable_Rbar_eq_le; apply measurable_gen; easy.
+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.
+Qed.
+
+Lemma measurable_Rbar_gt : forall b, measurable_Rbar (Rbar_gt b).
+Proof.
+intros; apply measurable_compl_rev.
+
+(* We need Rbar_le_not_gt. *)
+
+Admitted.
+
+Lemma measurable_Rbar_ge : forall b, measurable_Rbar (Rbar_ge b).
+Proof.
+intros; apply measurable_compl_rev.
+
+(* We need Rbar_lt_not_ge. *)
+
+Admitted.
+
+Lemma measurable_Rbar_oo : forall a b, measurable_Rbar (Rbar_oo a b).
+Proof.
+intros; apply measurable_inter.
+apply measurable_Rbar_lt.
+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.
+Qed.
+
+Lemma measurable_Rbar_co : forall a b, measurable_Rbar (Rbar_co a b).
+Proof.
+intros; apply measurable_inter.
+apply measurable_Rbar_le.
+apply measurable_Rbar_gt.
+Qed.
+
+Lemma measurable_Rbar_cc : forall a b, measurable_Rbar (Rbar_cc a b).
+Proof.
+intros; apply measurable_inter.
+apply measurable_Rbar_le.
+apply measurable_Rbar_ge.
+Qed.
+
 End measurable_Rbar.