Proofs of measurable_Rbar_topo_basis_gt and measurable_Rbar_topo_basis_lt.

Lebesgue/measurable_Rbar.v

@@ -14,11 +14,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import Qreals Reals Lra.
+From Coq Require Import Lia Qreals Reals Lra.
 From Coquelicot Require Import Hierarchy Rbar.
 
-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 nat_compl countable_sets.
+Require Import Rbar_compl UniformSpace_compl topo_bases_R.
+Require Import Subset Subset_dec Subset_seq Subset_Rbar.
 Require Import Subset_system_base Subset_system.
 Require Import measurable measurable_R.
 
@@ -337,7 +338,30 @@ Qed.
 Lemma measurable_Rbar_topo_basis_gt :
   forall (b : R), measurable gen_Rbar_topo_basis (Rbar_gt b).
 Proof.
-Admitted.
+intros b; apply measurable_ext with
+    (union_seq (fun n => let qn := Q2R (bij_NQ n) in
+       inter (Prop_cst (Rbar_gt b qn)) (Rbar_gt qn))).
+(* *)
+intros y; split.
+intros [n [Hn1 Hn2]]; apply Rbar_lt_trans with (Q2R (bij_NQ n)); easy.
+intros Hb; destruct y as [x | | ]; simpl; try easy.
+destruct (Q_dense _ _ Hb) as [q Hq].
+exists (bij_QN q); rewrite bij_NQN; split; easy.
+destruct (Q_dense (b - 1) b) as [q [_ Hq]]; try lra.
+exists (bij_QN q); rewrite bij_NQN; split; easy.
+(* *)
+apply measurable_union_seq; intros k;
+    apply measurable_inter; [apply measurable_Prop | apply measurable_gen].
+pose (m := (2 * k + 1)%nat). pose (n := (2 * m)%nat).
+rewrite subset_ext with (B := topo_basis_Rbar n); try easy.
+unfold topo_basis_Rbar; destruct (Even_Odd_dec n) as [Hk1 | Hk1].
+destruct (Even_Odd_dec (Nat.div2 n)) as [Hk2 | Hk2];
+    unfold n, m in *; rewrite Nat.div2_double in *.
+destruct (Nat.Even_Odd_False _ Hk2); exists k; easy.
+replace (2 * k + 1 - 1)%nat with (2 * k)%nat; try lia.
+rewrite Nat.div2_double; easy.
+destruct (Nat.Even_Odd_False n); try easy; exists m; easy.
+Qed.
 
 Lemma measurable_Rbar_Borel_eq_gt :
   measurable_Rbar_Borel = measurable gen_Rbar_gt.
@@ -391,7 +415,29 @@ Qed.
 Lemma measurable_Rbar_topo_basis_lt :
   forall (a : R), measurable gen_Rbar_topo_basis (Rbar_lt a).
 Proof.
-Admitted.
+intros a; apply measurable_ext with
+    (union_seq (fun n => let qn := Q2R (bij_NQ n) in
+       inter (Prop_cst (Rbar_lt a qn)) (Rbar_lt qn))).
+(* *)
+intros y; split.
+intros [n [Hn1 Hn2]]; apply Rbar_lt_trans with (Q2R (bij_NQ n)); easy.
+intros Ha; destruct y as [x | | ]; simpl; try easy.
+destruct (Q_dense _ _ Ha) as [q Hq].
+exists (bij_QN q); rewrite bij_NQN; split; easy.
+destruct (Q_dense a (a + 1)) as [q [Hq _]]; try lra.
+exists (bij_QN q); rewrite bij_NQN; split; try easy.
+(* *)
+apply measurable_union_seq; intros k;
+    apply measurable_inter; [apply measurable_Prop | apply measurable_gen].
+pose (m := (2 * k)%nat). pose (n := (2 * m)%nat).
+rewrite subset_ext with (B := topo_basis_Rbar n); try easy.
+unfold topo_basis_Rbar; destruct (Even_Odd_dec n) as [Hk1 | Hk1].
+destruct (Even_Odd_dec (Nat.div2 n)) as [Hk2 | Hk2];
+    unfold n, m in *; rewrite Nat.div2_double in *.
+rewrite Nat.div2_double; easy.
+destruct (Nat.Even_Odd_False m); try easy; exists k; easy.
+destruct (Nat.Even_Odd_False n); try easy; exists m; easy.
+Qed.
 
 Lemma measurable_Rbar_Borel_eq_lt :
   measurable_Rbar_Borel = measurable gen_Rbar_lt.