From 41809e6c035b4767fae4b2cf81a52e1b714af742 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 22 Mar 2022 20:11:45 +0100
Subject: [PATCH] WIP: other generators of measurable_Rbar_Borel.

---
 Lebesgue/measurable_Rbar.v | 238 +++++++++++++++----------------------
 1 file changed, 97 insertions(+), 141 deletions(-)

diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v
index 0414e869..7da98d6c 100644
--- a/Lebesgue/measurable_Rbar.v
+++ b/Lebesgue/measurable_Rbar.v
@@ -255,153 +255,38 @@ Inductive gen_Rbar_topo_basis : (Rbar -> Prop) -> Prop :=
 End gen_Rbar_Def.
 
 
-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_m_G : (Rbar -> Prop) -> Prop :=
-  UG_m : forall A, G A -> Up_m_G (up_m A).
-
-Hypothesis measurable_Up_m_G_singleton :
-  forall y, measurable Up_m_G (singleton y).
-
-Lemma measurable_Rbar_gen_lub_up_m :
-  Incl (measurable G) (fun A => measurable Up_m_G (up_m A)).
-Proof.
-intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
-apply measurable_gen; easy.
-apply measurable_union; try easy.
-rewrite up_id_empty; apply measurable_empty.
-rewrite up_m_compl; apply measurable_compl.
-apply measurable_union; try easy.
-apply measurable_ext with (diff (up_m A) (singleton m_infty)).
-Rbar_subset_full_unfold; intros y; destruct y; simpl; repeat split;
-    intros; try easy; tauto.
-apply measurable_diff; easy.
-rewrite up_m_union_seq; apply measurable_union_seq; easy.
-Qed.
-
-Inductive Up_p_G : (Rbar -> Prop) -> Prop :=
-  UG_p : forall A, G A -> Up_p_G (up_p A).
-
-Hypothesis measurable_Up_p_G_singleton :
-  forall y, measurable Up_p_G (singleton y).
-
-Lemma measurable_Rbar_gen_lub_up_p :
-  Incl (measurable G) (fun A => measurable Up_p_G (up_p A)).
-Proof.
-intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
-apply measurable_gen; easy.
-apply measurable_union; try easy.
-rewrite up_id_empty; apply measurable_empty.
-rewrite up_p_compl; apply measurable_compl.
-apply measurable_union; try easy.
-apply measurable_ext with (diff (up_p A) (singleton p_infty)).
-Rbar_subset_full_unfold; intros y; destruct y; simpl; repeat split;
-    intros; try easy; tauto.
-apply measurable_diff; easy.
-rewrite up_p_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_Rbar_Borel_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_Rbar_R_alt :
+(* WIP: alternate path...
+Lemma measurable_Rbar_R_alt_incl_lt :
   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.
-
 Admitted.
 
-Lemma measurable_Rbar_R_lt_alt :
-  Incl (measurable gen_Rbar_lt) measurable_Rbar_R.
+Lemma measurable_Rbar_R_eq_lt :
+  measurable_Rbar_R = measurable gen_Rbar_lt.
 Proof.
+apply Ext_equiv; split.
+(* *)
+unfold measurable_Rbar_R; rewrite measurable_R_eq_lt; intros B HB.
+admit.
+(* *)
 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.
+Admitted.
 
 Lemma measurable_Rbar_Borel_eq_lt :
   measurable_Rbar_Borel = measurable gen_Rbar_lt.
 Proof.
-apply Ext_equiv; split.
-rewrite <- measurable_Rbar_R_alt_correct; apply measurable_Rbar_lt_Rbar_R_alt.
-rewrite <- measurable_Rbar_R_correct; apply measurable_Rbar_R_lt_alt.
+rewrite <- measurable_Rbar_R_correct.
+apply measurable_Rbar_R_eq_lt.
 Qed.
+*)
 
 Lemma gen_Rbar_topo_basis_empty : gen_Rbar_topo_basis emptyset.
 Proof.
@@ -433,13 +318,29 @@ 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).
+Lemma measurable_Rbar_gt_le :
+  forall (a : R), measurable gen_Rbar_gt (Rbar_le a).
+Proof.
+intros; apply measurable_ext with (compl (Rbar_gt a)).
+split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
+apply measurable_compl, measurable_gen; easy.
+Qed.
+
+Lemma measurable_Rbar_gt_lt :
+  forall (a : R), measurable gen_Rbar_gt (Rbar_lt a).
+Proof.
+intros a; apply measurable_ext with (union_seq (Rbar_le_eps a)).
+rewrite Rbar_lt_is_Rbar_le_union_seq; easy.
+apply measurable_union_seq; intro; apply measurable_Rbar_gt_le.
+Qed.
+
+Lemma measurable_Rbar_topo_basis_gt :
+  forall (b : R), measurable gen_Rbar_topo_basis (Rbar_gt b).
 Proof.
 Admitted.
 
-Lemma measurable_Rbar_Borel_eq_lt' :
-  measurable_Rbar_Borel = measurable gen_Rbar_lt.
+Lemma measurable_Rbar_Borel_eq_gt :
+  measurable_Rbar_Borel = measurable gen_Rbar_gt.
 Proof.
 rewrite measurable_Rbar_Borel_eq_topo_basis.
 apply measurable_gen_ext; intros B HB.
@@ -447,28 +348,83 @@ apply measurable_gen_ext; intros B HB.
 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.
+2,4: apply measurable_gen; easy.
+1,2: apply measurable_Rbar_gt_lt; easy.
 (* *)
 induction HB as [a].
-apply measurable_gen.
-
-Admitted.
+apply measurable_Rbar_topo_basis_gt.
+Qed.
 
 Lemma measurable_Rbar_Borel_eq_le :
   measurable_Rbar_Borel = measurable gen_Rbar_le.
 Proof.
-Admitted.
+rewrite measurable_Rbar_Borel_eq_gt.
+apply measurable_gen_ext; intros B HB.
+(* *)
+induction HB as [b].
+apply measurable_ext with (compl (Rbar_le b)).
+split; [apply Rbar_not_le_lt | apply Rbar_lt_not_le].
+apply measurable_compl, measurable_gen; easy.
+(* *)
+induction HB as [a].
+apply measurable_ext with (compl (Rbar_gt a)).
+split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
+apply measurable_compl, measurable_gen; easy.
+Qed.
 
-Lemma measurable_Rbar_Borel_eq_gt :
-  measurable_Rbar_Borel = measurable gen_Rbar_gt.
+Lemma measurable_Rbar_lt_ge :
+  forall (b : R), measurable gen_Rbar_lt (Rbar_ge b).
+Proof.
+intros; apply measurable_ext with (compl (Rbar_lt b)).
+split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
+apply measurable_compl, measurable_gen; easy.
+Qed.
+
+Lemma measurable_Rbar_lt_gt :
+  forall (b : R), measurable gen_Rbar_lt (Rbar_gt b).
+Proof.
+intros b; apply measurable_ext with (union_seq (Rbar_ge_eps b)).
+rewrite Rbar_gt_is_Rbar_ge_union_seq; easy.
+apply measurable_union_seq; intro; apply measurable_Rbar_lt_ge.
+Qed.
+
+Lemma measurable_Rbar_topo_basis_lt :
+  forall (a : R), measurable gen_Rbar_topo_basis (Rbar_lt a).
 Proof.
 Admitted.
 
+Lemma measurable_Rbar_Borel_eq_lt :
+  measurable_Rbar_Borel = measurable gen_Rbar_lt.
+Proof.
+rewrite measurable_Rbar_Borel_eq_topo_basis.
+apply measurable_gen_ext; intros B HB.
+(* *)
+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_Rbar_topo_basis_lt.
+Qed.
+
 Lemma measurable_Rbar_Borel_eq_ge :
   measurable_Rbar_Borel = measurable gen_Rbar_ge.
 Proof.
-Admitted.
+rewrite measurable_Rbar_Borel_eq_lt.
+apply measurable_gen_ext; intros B HB.
+(* *)
+induction HB as [a].
+apply measurable_ext with (compl (Rbar_ge a)).
+split; [apply Rbar_not_le_lt | apply Rbar_lt_not_le].
+apply measurable_compl, measurable_gen; easy.
+(* *)
+induction HB as [b].
+apply measurable_ext with (compl (Rbar_lt b)).
+split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
+apply measurable_compl, measurable_gen; easy.
+Qed.
 
 End measurable_Rbar_Borel_eq.
 
-- 
GitLab