Module mathcomp.analysis.borel_hierarchy

From mathcomp Require Import boot order algebra.
From mathcomp Require Import boolp classical_sets functions cardinality.
From mathcomp Require Import reals topology normedtype sequences.
From mathcomp Require Import measure lebesgue_measure measurable_realfun.

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

Unset SsrOldRewriteGoalsOrder.
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 { : topologicalType}.
Implicit Type S : set T.

Definition :=
exists2 : (set T)^nat, (forall , open (F i)) & S = \bigcap_ (F i).

Lemma : open S -> Gdelta S.

Proof.

by exists (fun=> S)=> //; rewrite bigcap_const. Qed.

Definition :=
  exists2 : (set T)^nat,
    (forall , open (F i) /\ dense (F i)) & S = \bigcap_ (F i).

Definition :=
  exists2 : (set T)^nat, (forall , closed (F i)) & S = \bigcup_ (F i).

Lemma : closed S -> Fsigma S.

Proof.

by exists (fun=> S)=> //; rewrite bigcup_const. Qed.

End Gdelta_Fsigma.

Import MeasurableR.

Lemma { : realType} ( : set R) : Gdelta S -> measurable S.

Proof.

move=> [] B oB ->; apply: bigcapT_measurable => i.
exact: open_measurable.
Qed.

Lemma { : realType} ( : set R) ( : set (subspace A)) :
open A -> Gdelta S -> Gdelta (A `&` S).

Proof.

move=> oA [/= S_ oS_ US]; exists (fun => A `&` (S_ n)).
by move=> ?; rewrite open_setSI.
by rewrite bigcapIr// US.
Qed.

Section irrational_Gdelta.
Context { : realType}.

Lemma : 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 => ~` [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 ( : 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 => A n `&` B n.
have C0 : set0 = \bigcap_ C i by rewrite bigcapI -ratrA -irratB setICr.
have /Baire : forall , 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.

Files

Module mathcomp.analysis.borel_hierarchy