From 4abd489e0bf4921dcb68fe2d8bc601e49ba5b84c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr> Date: Fri, 11 Mar 2022 19:56:35 +0100 Subject: [PATCH] WIP: proofs of measurable_Borel_Rbar_eq_(l|g)(t|e). Proofs of measurable_Rbar_*. --- Lebesgue/measurable_Rbar.v | 384 ++++++++++++++++++++++++++++++------- 1 file changed, 317 insertions(+), 67 deletions(-) diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v index 1603f640..fb00a657 100644 --- a/Lebesgue/measurable_Rbar.v +++ b/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. -- GitLab