diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c8e87625e..677f15701 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,8 +18,26 @@ - in `exp.v: + lemma `norm_expR` +- in `reals.v`: + + definition `irrational` + + lemmas `irrationalE`, `rationalP` + +- in `topology_structure.v`: + + lemmas `denseI`, `dense0` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `dense_set1C` + +- new file `borel_hierarchy.v`: + + definitions `Gdelta`, `Fsigma` + + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`, + `irrational_Gdelta`, `not_rational_Gdelta` + ### Changed +- moved from `pi_irrational.v` to `reals.v` and changed + + definition `rational` + ### Renamed - in `lebesgue_stieltjes_measure.v`: diff --git a/_CoqProject b/_CoqProject index 7feb87c50..47e426cfc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -96,6 +96,7 @@ theories/lebesgue_stieltjes_measure.v theories/derive.v theories/measure.v theories/numfun.v +theories/borel_hierarchy.v theories/lebesgue_integral_theory/simple_functions.v theories/lebesgue_integral_theory/lebesgue_integral_definition.v diff --git a/reals/reals.v b/reals/reals.v index 974c5d10a..a400ee645 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -36,6 +36,11 @@ (* Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) *) (* ``` *) (* *) +(* ``` *) +(* @rational R == set of rational numbers of type R : realType *) +(* @irrational R == the complement of rational R *) +(* ``` *) +(* *) (******************************************************************************) From Corelib Require Import Setoid. @@ -708,3 +713,33 @@ by rewrite 2!ratr_int mulr_natr (le_lt_trans _ c). Qed. End rat_in_itvoo. + +Section rational. +Context {R : realType}. + +Definition rational : set R := ratr @` [set: rat]. + +Lemma rationalP (r : R) : + rational r <-> exists (a : int) (b : nat), r = a%:~R / b%:R. +Proof. +split=> [[q _ <-{r}]|[a [b ->]]]; last first. + exists (a%:~R / b%:R) => //. + by rewrite ratr_is_multiplicative ratr_int fmorphV//= ratr_nat. +have [n d nd] := ratP q. +have [n0|n0] := leP 0 n. + exists n, d.+1. + by rewrite ratr_is_multiplicative ratr_int fmorphV/= ratr_nat. +exists (- `|n|), d.+1. +by rewrite ratr_is_multiplicative ltr0_norm// opprK fmorphV//= !ratr_int. +Qed. + +Definition irrational : set R := ~` rational. + +Lemma irrationalE : irrational = \bigcap_(q : rat) ~` (ratr @` [set q]). +Proof. +apply/seteqP; split => [r/= rE q _/=|r/= rE [q] _ qr]; last first. + by apply: (rE q Logic.I) => /=; exists q. +by apply: contra_not rE => -[_ -> <-{r}]; exists q. +Qed. + +End rational. diff --git a/theories/Make b/theories/Make index d80af9e6f..77ba62671 100644 --- a/theories/Make +++ b/theories/Make @@ -60,6 +60,7 @@ lebesgue_measure.v derive.v measure.v numfun.v +borel_hierarchy.v lebesgue_integral_theory/simple_functions.v lebesgue_integral_theory/lebesgue_integral_definition.v diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v new file mode 100644 index 000000000..6bd0622ea --- /dev/null +++ b/theories/borel_hierarchy.v @@ -0,0 +1,96 @@ +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop interval_inference. +From mathcomp Require Import reals ereal topology normedtype sequences. +From mathcomp Require Import real_interval numfun esum measure lebesgue_measure. + +(**md**************************************************************************) +(* # Basic facts about G-delta and F-sigma sets *) +(* *) +(* ``` *) +(* Gdelta S == S is countable intersection of open sets *) +(* Gdelta_dense S == S is a countable intersection of dense open sets *) +(* Fsigma S == S is countable union of closed sets *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. + +Section Gdelta_Fsigma. +Context {T : topologicalType}. +Implicit Type S : set T. + +Definition Gdelta S := + exists2 F : (set T)^nat, (forall i, open (F i)) & S = \bigcap_i (F i). + +Lemma open_Gdelta S : open S -> Gdelta S. +Proof. by exists (fun=> S)=> //; rewrite bigcap_const. Qed. + +Definition Gdelta_dense S := + exists2 F : (set T)^nat, + (forall i, open (F i) /\ dense (F i)) & S = \bigcap_i (F i). + +Definition Fsigma S := + exists2 F : (set T)^nat, (forall i, closed (F i)) & S = \bigcup_i (F i). + +Lemma closed_Fsigma S : closed S -> Fsigma S. +Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed. + +End Gdelta_Fsigma. + +Lemma Gdelta_measurable {R : realType} (S : set R) : Gdelta S -> measurable S. +Proof. +move=> [] B oB ->; apply: bigcapT_measurable => i. +exact: open_measurable. +Qed. + +Lemma Gdelta_subspace_open {R : realType} (A : set R) (S : set (subspace A)) : + open A -> Gdelta S -> Gdelta (A `&` S). +Proof. +move=> oA [/= S_ oS_ US]; exists (fun n => A `&` (S_ n)). + by move=> ?; rewrite open_setSI. +by rewrite bigcapIr// US. +Qed. + +Section irrational_Gdelta. +Context {R : realType}. + +Lemma irrational_Gdelta : Gdelta_dense (@irrational R). +Proof. +rewrite irrationalE. +have /pcard_eqP/bijPex[f bijf] := card_rat. +pose f1 := 'pinv_(fun => 0%R) [set: rat] f. +exists (fun n => ~` [set ratr (f1 n)]). + move=> n; rewrite openC; split; last exact: dense_set1C. + exact/accessible_closed_set1/hausdorff_accessible/Rhausdorff. +apply/seteqP; split => [/= r/= rE n _/= rf1n|/=r rE q _/= [_ -> qr]]. + by apply: (rE (f1 n)) => //=; exists (f1 n). +apply: (rE (f q)) => //=. +by rewrite /f1 pinvKV ?inE//=; exact: set_bij_inj bijf. +Qed. + +End irrational_Gdelta. + +Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R). +Proof. +apply/forall2NP => A; apply/not_andP => -[oA ratrA]. +have dense_A n : dense (A n). + move=> D D0 /(@dense_rat R D D0); apply/subset_nonempty; apply: setIS. + by rewrite -/(@rational R) ratrA; exact: bigcap_inf. +have [/= B oB irratB] := @irrational_Gdelta R. +pose C : (set R)^nat := fun n => A n `&` B n. +have C0 : set0 = \bigcap_i C i by rewrite bigcapI -ratrA -irratB setICr. +have /Baire : forall n, open (C n) /\ dense (C n). + move=> n; split. + - by apply: openI => //; apply oB. + - by apply: denseI => //; apply oB. +by rewrite -C0; exact: dense0. +Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 48005b39b..30e6d7511 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -859,6 +859,22 @@ Qed. End open_itv_subset. +Lemma dense_set1C {R : realType} (r : R) : dense (~` [set r]). +Proof. +move=> /= O O0 oO. +suff [s Os /eqP sr] : exists2 s, O s & s != r by exists s; split. +case: O0 => o Oo. +have [->{r}|ro] := eqVneq r o; last by exists o => //; rewrite eq_sym. +have [e' /= e'0 e'o] := open_itvoo_subset oO Oo. +near (0:R)^'+ => e. +exists (o + e/2)%R; last by rewrite gt_eqF// ltrDl// divr_gt0. +apply: (e'o e) => //=. + by rewrite sub0r normrN gtr0_norm. +rewrite in_itv/= !ltrD2l; apply/andP; split. + by rewrite (@lt_le_trans _ _ 0%R) ?divr_ge0// ltrNl oppr0. +by rewrite gtr_pMr// invf_lt1// ltr1n. +Unshelve. all: by end_near. Qed. + Section pseudoMetricNormedZmod_numFieldType. Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). Variables (I : Type) (F : set_system I) (FF : Filter F) (f : I -> V) (y : V). diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index fd0817328..8a505c374 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -28,9 +28,6 @@ apply/measurable_funTS; apply: continuous_measurable_fun. exact/continuous_horner. Qed. -(* TODO: move somewhere to classical *) -Definition rational {R : realType} (x : R) := exists m n, x = (m%:~R / n%:R)%R. - Module pi_irrational. Local Open Scope ring_scope. @@ -409,10 +406,10 @@ End pi_irrational. Lemma pi_irrationnal {R : realType} : ~ rational (pi : R). Proof. -move=> [a [b]]; have [->|b0 piratE] := eqVneq b O. +move/rationalP => [a [b]]; have [->|b0 piratE] := eqVneq b O. by rewrite invr0 mulr0; apply/eqP; rewrite gt_eqF// pi_gt0. -have [na ana] : exists na, (a%:~R = na %:R :> R)%R. - exists `|a|; rewrite natr_absz gtr0_norm//. +have [na ana] : exists na, (a%:~R = na%:R :> R)%R. + exists `|a|%N; rewrite natr_absz gtr0_norm//. by have := @pi_gt0 R; rewrite piratE pmulr_lgt0 ?invr_gt0 ?ltr0n ?lt0n// ltr0z. rewrite {}ana in piratE. have [N _] := pi_irrational.intfsin_small b0 (esym piratE) (@ltr01 R). diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 88d9b539e..cc1621662 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -935,6 +935,23 @@ move=> /existsNP[X /not_implyP[[x Xx] /not_implyP[ Ox /forallNP A]]]. by exists X; split; [exists x | rewrite -subset0; apply/A]. Qed. +Lemma denseI (T : topologicalType) (A B : set T) : + open A -> dense A -> dense B -> dense (A `&` B). +Proof. +move=> oA dA dB C C0 oC. +have CA0 : C `&` A !=set0 by exact: dA. +suff: (C `&` A) `&` B !=set0 by rewrite setIA. +by apply: dB => //; exact: openI. +Qed. + +Lemma dense0 {R : ptopologicalType} : ~ dense (@set0 R). +Proof. +apply/existsNP; exists setT. +apply/not_implyP; split; first exact/set0P/setT0. +apply/not_implyP; split; first exact: openT. +by rewrite setTI => -[]. +Qed. + Section ClopenSets. Implicit Type T : topologicalType.