basic facts about Gdelta sets

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`:

_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

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.

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

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.

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).

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).

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.