move rational definitions into reals.v

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,6 @@
 
 ### Added
 
-### Changed
-
 - in `sequences.v`:
   + lemma `subset_seqDU`
 
@@ -17,13 +15,23 @@
   + lemma `ae_foralln`
   + lemma `ae_eqe_mul2l`
 
+- in `reals.v`:
+  + definition `irrational`
+  + lemmas `irrationalE`, `rationalP` 
+
+- file `borel_hierarchy.v`:
+  + lemmas ``
+
 ### Changed
 
 - in `measure.v`:
   + notation `{ae mu, P}` (near use `{near _, _}` notation)
   + definition `ae_eq`
   + `ae_eq` lemmas now for `ringType`-valued functions (instead of `\bar R`)
 
+- moved from `pi_irrational.v` to `reals.v` and changed
+  + definition `rational`
+
 ### Renamed
 
 ### Generalized

theories/Make

@@ -60,6 +60,7 @@ forms.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

@@ -5,8 +5,12 @@ From mathcomp Require Import reals ereal topology normedtype sequences.
 From mathcomp Require Import real_interval esum measure lebesgue_measure numfun.
 
 (**md**************************************************************************)
+(* # Basic facts about G-delta and F-sigma sets                               *)
+(*                                                                            *)
 (* ```                                                                        *)
-(*   Gdelta S == S is a set of countable intersection of open 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                    *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -20,17 +24,21 @@ Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 
-Definition irrational (R : realType) : set R := ~` (ratr @` [set: rat]).
-Arguments irrational : clear implicits.
-
-Definition rational (R : realType) : set R := (ratr @` [set: rat]).
+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 irratE (R : realType) :
-  irrational R = \bigcap_(q : rat) ~` (ratr @` [set q]).
+Lemma dense0 {R : ptopologicalType} : ~ dense (@set0 R).
 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.
+apply/existsNP; exists setT.
+apply/not_implyP; split; first exact/set0P/setT0.
+apply/not_implyP; split; first exact: openT.
+by rewrite setTI => -[].
 Qed.
 
 Lemma dense_set1C {R : realType} (r : R) : dense (~` [set r]).
@@ -49,53 +57,49 @@ rewrite in_itv/= !ltrD2l; apply/andP; split.
 by rewrite gtr_pMr// invf_lt1// ltr1n.
 Unshelve. all: by end_near. 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.
+Section Gdelta_Fsigma.
+Context {T : topologicalType}.
+Implicit Type S : set T.
 
-Lemma dense0 {R : realType} : ~ 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.
+Definition Gdelta S :=
+  exists2 F : (set T)^nat, (forall i, open (F i)) & S = \bigcap_i (F i).
 
-Section Fsigma.
+Lemma open_Gdelta S : open S -> Gdelta S.
+Proof. by exists (fun=> S)=> //; rewrite bigcap_const. Qed.
 
-Definition Fsigma (R : topologicalType) (S : set R) :=
-  exists2 A_ : (set R)^nat,
- (forall i : nat, closed (A_ i)) & S = \bigcup_i (A_ i).
+Definition Gdelta_dense S :=
+  exists2 F : (set T)^nat,
+    (forall i, open (F i) /\ dense (F i)) & S = \bigcap_i (F i).
 
-Lemma closed_Fsigma (R : topologicalType) (S : set R) : closed S -> Fsigma S.
-Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed.
+Definition Fsigma S :=
+  exists2 F : (set T)^nat, (forall i, closed (F i)) & S = \bigcup_i (F i).
 
-End Fsigma.
+Lemma closed_Fsigma S : closed S -> Fsigma S.
+Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed.
 
-Section Gdelta.
+End Gdelta_Fsigma.
 
-Definition Gdelta (R : topologicalType) (S : set R) :=
-  exists2 A_ : (set R)^nat,
- (forall i : nat, open (A_ i)) & S = \bigcap_i (A_ i).
+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 open_Gdelta (R : topologicalType) (S : set R) : open S -> Gdelta S.
-Proof. by exists (fun=> S)=> //; rewrite bigcap_const. 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 irrat_Gdelta.
+Section irrational_Gdelta.
 Context {R : realType}.
 
-Definition Gdelta_dense (R : topologicalType) (S : set R) :=
-  exists2 A_ : (set R)^nat,
-  (forall i, open (A_ i) /\ dense (A_ i)) & S = \bigcap_i (A_ i).
-
-Lemma irrat_Gdelta : Gdelta_dense (irrational R).
+Lemma irrational_Gdelta : Gdelta_dense (irrational R).
 Proof.
-rewrite irratE.
+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)]).
@@ -110,9 +114,9 @@ rewrite /f1 pinvKV ?inE//=.
 exact: set_bij_inj bijf.
 Qed.
 
-End irrat_Gdelta.
+End irrational_Gdelta.
 
-Lemma rat_not_Gdelta (R : realType) : ~ Gdelta (@rational R).
+Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R).
 Proof.
 apply/forall2NP => A.
 apply/not_andP => -[oA ratrA].
@@ -123,10 +127,9 @@ have dense_A n : dense (A n).
   apply: setIS.
   rewrite -/(@rational R) ratrA.
   exact: bigcap_inf.
-have [/= B oB irratB] := @irrat_Gdelta R.
+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 C0 : set0 = \bigcap_i C i by rewrite bigcapI -ratrA -irratB setICr.
 have : forall n, open (C n) /\ dense (C n).
   move=> n; split.
     by apply: openI => //; apply oB.
@@ -135,18 +138,3 @@ move/Baire.
 rewrite -C0.
 exact: dense0.
 Qed.
-
-Lemma Gdelta_measurable {R : realType} (S : set R) : Gdelta S -> (@measurable _ R) 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 R (A `&` S).
-Proof.
-move=> oA [/= S_ oS_ US].
-exists (fun n => A `&` (S_ n)).
-  by move=> ?; rewrite open_setSI.
-by rewrite bigcapIr// US.
-Qed.

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,7 +406,7 @@ 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//.