Sorgenfrey line and properties

_CoqProject

@@ -30,7 +30,6 @@ reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
 reals/signed.v
-reals/interval_inference.v
 reals/prodnormedzmodule.v
 reals/all_reals.v
 experimental_reals/xfinmap.v
@@ -120,5 +119,6 @@ theories/kernel.v
 theories/pi_irrational.v
 theories/gauss_integral.v
 theories/showcase/summability.v
+theories/showcase/sorgenfreyline.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/all_reals.v

@@ -1,4 +1,3 @@
-From mathcomp Require Export interval_inference.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
 From mathcomp Require Export real_interval.

reals/reals.v

@@ -43,7 +43,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Corelib Require Import Setoid.
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.

theories/Make

@@ -86,3 +86,4 @@ pi_irrational.v
 gauss_integral.v
 all_analysis.v
 showcase/summability.v
+showcase/sorgenfreyline.v

theories/borel_hierarchy.v

@@ -19,10 +19,13 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.TTheory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory Num.Def.
 Import numFieldNormedType.Exports.
+Import numFieldTopology.Exports.
+Import exp.
 
 Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
 
 Section Gdelta_Fsigma.
 Context {T : topologicalType}.
@@ -94,3 +97,302 @@ have /Baire : forall n, open (C n) /\ dense (C n).
   - by apply: denseI => //; apply oB.
 by rewrite -C0; exact: dense0.
 Qed.
+
+Section perfectlynormalspace.
+Context (R : realType) (T : topologicalType).
+
+Definition perfectly_normal_space (x : R) :=
+  forall E : set T, closed E -> 
+    exists f : T -> R, continuous f /\ E = f @^-1` [set x].
+
+Lemma perfectly_normal_spaceP x y : perfectly_normal_space x -> perfectly_normal_space y.
+Proof.
+move=>px E cE.
+case:(px E cE) => f [] cf ->.
+pose f' := f + cst (y - x). 
+exists f'.
+split.
+  rewrite /f'.
+  move=> z.
+  apply: continuousD.
+    exact:cf.
+  exact:cst_continuous.
+apply/seteqP.
+rewrite /f' /cst /=.
+split => z /=.
+  rewrite addrfctE => ->.
+  by rewrite subrKC.
+rewrite addrfctE.
+move/eqP.
+by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP.
+Qed.
+
+Definition perfectly_normal_space' (x : R) :=
+  forall E : set T, open E -> 
+    exists f : T -> R, continuous f /\ E = f @^-1` ~`[set x].
+
+Definition perfectly_normal_space01 :=
+  forall E F : set T, closed E -> closed F -> [disjoint E & F] ->
+    exists f : T -> R,
+      [/\ continuous f, E = f @^-1` [set 0], F = f @^-1` [set 1]
+        & range f `<=` `[0, 1]%classic].
+
+Definition perfectly_normal_space_Gdelta :=
+  normal_space T /\ forall E : set T, closed E -> Gdelta E.
+
+Lemma perfectly_normal_space01_normal :
+  perfectly_normal_space01 -> normal_space T.
+Proof.
+move=> pns01.
+rewrite (@normal_separatorP R).
+move=> A B cA cB /eqP AB.
+apply/uniform_separatorP.
+have[f [] cf Af Bf f01] := pns01 _ _ cA cB AB.
+exists f.
+by split => //; rewrite (Af, Bf); exact:image_preimage_subset.
+Qed.
+
+Lemma EFin_series (f : R^nat) : EFin \o series f = eseries (EFin \o f).
+Proof.
+apply/boolp.funext => n.
+rewrite /series /eseries /=.
+elim: n => [|n IH]; first by rewrite !big_geq.
+by rewrite !big_nat_recr //= EFinD IH.
+Qed.
+
+Local Lemma perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space 0.
+Proof.
+move=> pnsGd E cE.
+case: (pnsGd) => nT cEGdE.
+have[U oU HE]:= cEGdE E cE.
+have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, 
+  [/\ continuous f, range f `<=` `[0, 1], f @` E `<=` [set 0] & f @` (~` U n) `<=` [set 1]].
+  move=> n.
+  apply/uniform_separatorP.
+  apply: normal_uniform_separator => //.
+  - by rewrite closedC.
+  - rewrite HE -subsets_disjoint.
+    exact: bigcap_inf.
+have f_n_ge0 i y : 0 <= f_n i y.
+    case: (Hn i) => _ Hr _ _.
+    have /Hr /= := imageT (f_n i) y.
+    by rewrite in_itv /= => /andP[].
+have f_n_le1 i y : f_n i y <= 1.
+    case: (Hn i) => _ Hr _ _.
+    have /Hr /= := imageT (f_n i) y.
+    by rewrite in_itv /= => /andP[].
+pose f_sum := fun n => \sum_(0 <= k < n) (f_n k \* cst (2^-k.+1)).
+have cf_sum n : continuous (f_sum n).
+  rewrite /f_sum => x; elim: n => [|n IH].
+    rewrite big_geq //; exact: cst_continuous.
+  rewrite big_nat_recr //=; apply: continuousD => //.
+  apply/continuousM/cst_continuous.
+  by case: (Hn n) => /(_ x).
+have f_sumE x n : f_sum n x = [series f_n k x * 2^-k.+1]_k n
+  by exact: (big_morph (@^~ x)).
+have f_sumE' x := boolp.funext (f_sumE x).
+pose f := fun x => limn (f_sum^~ x); rewrite /= in f.
+exists f.
+have ndf_sum y : {homo f_sum^~ y : a b / (a <= b)%N >-> a <= b}.
+  move=> a b ab.
+  rewrite /f_sum (big_cat_nat _ ab) //= lerDl.
+  rewrite (big_morph (@^~ y) (id1:=0) (op1:=GRing.add)) //=.
+  rewrite sumr_ge0 // => i _.
+  by rewrite mulr_ge0 // invr_ge0 exprn_ge0.
+have Hcvg y : cvgn (f_sum^~ y).
+  apply: nondecreasing_is_cvgn => //.
+  exists 1 => z /= [m] _ <-.
+  have -> : 1 = 2^-1 / (1 - 2^-1) :> R.
+    rewrite -[LHS](@mulfV _ (2^-1)) //; congr (_ / _).
+    by rewrite [X in X - _](splitr 1) mul1r addrK.
+  rewrite f_sumE.
+  apply: le_trans (geometric_le_lim m _ _ _) => //; last first.
+    by rewrite ltr_norml (@lt_trans _ _ 0) //= invf_lt1 // ltr1n.
+  rewrite ler_sum // => i _.
+  by rewrite /geometric /= -exprS -exprVn ler_piMl.
+split.
+  move=> x Nfx.
+  rewrite -filter_from_ballE.
+  case => eps /= eps0 HB.
+  pose n := (2 + truncn (- ln eps / ln 2))%N.
+  have eps0' : eps / 2 > 0 by exact: divr_gt0.
+  move/continuousP/(_ _ (ball_open (f_sum n x) eps0')) : (cf_sum n) => /= ofs.
+  rewrite nbhs_filterE fmapE nbhsE /=.
+  set B := _ @^-1` _ in ofs.
+  exists B.
+    split => //; exact: ballxx.
+  apply: subset_trans (preimage_subset (f:=f) HB).
+  rewrite /B /preimage /ball => t /=.
+  have Hf y :
+    f y = f_sum n y + limn (fun n' => \sum_(n <= k < n') f_n k y * 2^- k.+1).
+    have /= := nondecreasing_telescope_sumey n _ (ndf_sum y).
+    rewrite EFin_lim // fin_numE /= => /(_ isT).
+    rewrite (eq_eseriesr (g:=fun i => ((f_n i \* cst (2 ^- i.+1)) y)%:E));
+      last first.
+      move => i _.
+      rewrite /f_sum -EFinD big_nat_recr //=.
+      by rewrite [X in X _ _ y]/GRing.add /= addrAC subrr add0r.
+    move/(f_equal (fun x => (f_sum n y)%:E + x)).
+    rewrite addrA addrAC -EFinB subrr add0r => H.
+    apply: EFin_inj.
+    rewrite -H EFinD; congr (_ + _).
+    rewrite -EFin_lim.
+      apply/congr_lim/boolp.funext => k /=.
+      exact/esym/big_morph.
+    by rewrite is_cvg_series_restrict -f_sumE'.
+  move=> feps.
+  rewrite !Hf opprD addrA (addrAC (f_sum n x)) -(addrA (_ - _)).
+  apply: (le_lt_trans (ler_normD _ _)).
+  rewrite (splitr eps).
+  apply: ltr_leD => //.
+  have Hfn y : 0 <= \big[+%R/0]_(n <= k <oo) (f_n k y / 2 ^+ k.+1) <= 2^-n.
+    apply/andP; split.
+      have := nondecreasing_cvgn_le (ndf_sum y) (Hcvg y) n.
+      by rewrite [limn _]Hf lerDl.
+    have H2n : 0 <= 2^-n :> R by rewrite -exprVn exprn_ge0.
+    rewrite -lee_fin.
+    apply: le_trans (epsilon_trick0 xpredT H2n).
+    rewrite -EFin_lim; last by rewrite is_cvg_series_restrict -f_sumE'.
+    under [EFin \o _]boolp.funext do
+      rewrite /= (big_morph EFin (id1:=0) (op1:=GRing.add)) //.
+    rewrite -nneseries_addn; last by move=> i; rewrite lee_fin mulr_ge0.
+    apply: lee_nneseries => i _.
+      by rewrite lee_fin mulr_ge0.
+    by rewrite lee_fin natrX -!exprVn -exprD addnS addnC ler_piMl.
+  have Hfn0 x := proj1 (elimT andP (Hfn x)).
+  have {Hfn}Hfn1 x := proj2 (elimT andP (Hfn x)).
+  apply: (@le_trans _ _ (2^-n)).
+    rewrite ler_norml !lerBDl (le_trans (Hfn1 t)) ?lerDl //=.
+    by rewrite (le_trans (Hfn1 x)) // lerDr.
+  rewrite /n -exprVn addSnnS exprD expr1 ler_pdivrMl //.
+  rewrite mulrA (mulrC 2) mulfK // -(@lnK _ (2^-1)) ?posrE //.
+  rewrite -expRM_natl -{2}(@lnK _ eps) // ler_expR lnV ?posrE //.
+  rewrite -ler_ndivrMr ?posrE; last by rewrite oppr_lt0 ln_gt0 // ltr1n.
+  by rewrite invrN mulrN mulNr ltW // truncnS_gt.
+apply/seteqP; split => x /= Hx.
+  apply: EFin_inj.
+  rewrite -EFin_lim // f_sumE' EFin_series /= eseries0 // => i _ _ /=.
+  case: (Hn i) => _ _ /(_ (f_n i x)) /= => ->.
+    by rewrite mul0r.
+  by exists x.
+apply: contraPP Hx.
+rewrite (_ : (~ E x) = setC E x) // HE setC_bigcap /= => -[] i _ HU.
+case: (Hn i) => _ _ _ /(_ (f_n i x)) /= => Hfix.
+rewrite /f => Hf.
+have := (nondecreasing_cvgn_le (ndf_sum x) (Hcvg x) i.+1).
+have := ndf_sum x _ _ (leq0n i.+1).
+rewrite Hf {1}/f_sum big_geq // => /[swap] fi_le0.
+rewrite le0r ltNge fi_le0 orbF.
+rewrite /f_sum big_nat_recr //= [X in X _ _ x]/GRing.add /= -/(f_sum i).
+rewrite Hfix; last by exists x.
+rewrite mul1r /cst => /eqP fi0.
+have := ndf_sum x _ _ (leq0n i).
+rewrite {1}/f_sum big_geq // -[0 x]fi0 gerDl.
+by rewrite leNgt invr_gt0 exprn_gt0.
+Qed.
+
+Local Lemma perfectly_normal_space_23 : perfectly_normal_space 0 -> perfectly_normal_space' 0.
+Proof.
+move=> pns' E cE; case: (pns' (~`E)).
+  by rewrite closedC.
+move=> f [cf f0]; exists f.
+split.
+  by [].
+by rewrite -[LHS]setCK f0 preimage_setC.
+Qed.
+
+Local Lemma perfectly_normal_space_32 : perfectly_normal_space' 0 -> perfectly_normal_space 0.
+Proof.
+move=> pns' E cE; case: (pns' (~`E)).
+  by rewrite openC.
+move=> f [cf f0]; exists f.
+split.
+  by [].
+by rewrite -[RHS]setCK preimage_setC -f0 setCK.
+Qed.
+
+(* (norm \o f) @^-1` [set 0] = f @^-1` [set 0] *)
+Lemma norm_preimage0 (f : T -> R) :
+  continuous f ->
+  exists f' : T -> R, [/\ continuous f', (forall x, f' x >= 0)
+                        & f' @^-1` [set 0] = f @^-1` [set 0]].
+Proof.
+move=> cf; exists (fun x => `|f x|); split => //.
+- move=> x; exact/continuous_comp/norm_continuous/cf.
+- apply/seteqP; split => [x|x /= ->]; [exact: normr0_eq0 | by rewrite normr0].
+Qed.
+
+Local Lemma perfectly_normal_space_24 : perfectly_normal_space 0 -> perfectly_normal_space01.
+Proof.
+move=> pns0 E F cE cF EF.
+have [_ [/norm_preimage0 [f [cf f_ge0 <-]] E0]] := pns0 E cE.
+have [_ [/norm_preimage0 [g [cg g_ge0 <-]] F0]] := pns0 F cF.
+have fg_gt0 x : f x + g x > 0.
+  move: (f_ge0 x) (g_ge0 x).
+  rewrite !le_eqVlt => /orP[/eqP|] Hf /orP[/eqP|] Hg; last exact: addr_gt0.
+  + by move: EF; rewrite E0 F0 => /disj_setPRL/(_ x); elim.
+  + by rewrite -Hf add0r.
+  + by rewrite -Hg addr0.
+have fg_neq0 x : f x + g x != 0 by apply: lt0r_neq0.
+exists (fun x => f x / (f x + g x)); split.
+- move=> x; apply: (continuousM (cf x)).
+  apply: continuous_comp; [exact/continuousD/cg/cf | exact: inv_continuous].
+- rewrite E0.
+  apply/seteqP; split => x /=; first by move->; rewrite mul0r.
+  move/(f_equal (GRing.mul ^~ (f x + g x))).
+  by rewrite -mulrA mulVf // mulr1 mul0r.
+- rewrite F0.
+  apply/seteqP; split => x /=.
+    rewrite -{1}(addr0 (f x)) => <-; exact: mulfV.
+  move/(f_equal (GRing.mul ^~ (f x + g x))).
+  rewrite -mulrA mulVf // mulr1 mul1r => /eqP.
+  by rewrite addrC -subr_eq subrr eq_sym => /eqP.
+- move=> _ [x] _ /= <-.
+  have fgx : (f x + g x)^-1 >= 0 by apply/ltW; rewrite invr_gt0.
+  by rewrite in_itv /= mulr_ge0 //= -(mulfV (fg_neq0 x)) ler_pM // lerDl.
+Qed.
+
+Local Lemma perfectly_normal_space_42 :                                 
+perfectly_normal_space01  -> perfectly_normal_space 0.                  
+Proof.                                                                  
+move=> + E cE => /(_ E set0 cE closed0).                                
+rewrite disj_set2E setI0 eqxx => /(_ erefl).                            
+case=> f [] cf [] Ef [] _ _.                                            
+by exists f; split.                                                     
+Qed.                                                                    
+
+Local Lemma perfectly_normal_space_41 :
+  perfectly_normal_space01 -> perfectly_normal_space_Gdelta.
+Proof.            
+move=> pns01; split; first exact: perfectly_normal_space01_normal.
+move=> E cE; case:(perfectly_normal_space_42 pns01 cE) => // f [] cf Ef.
+exists (fun n => f @^-1` `]-n.+1%:R^-1,n.+1%:R^-1[%classic).
+  by move=> n; move/continuousP: cf; apply; exact: itv_open.
+rewrite -preimage_bigcap (_ : bigcap _ _ = [set 0])//.
+rewrite eqEsubset; split; last first.
+  by move=> x -> n _ /=; rewrite in_itv//= oppr_lt0 andbb invr_gt0.
+apply: subsetC2; rewrite setC_bigcap => x /= /eqP x0.
+exists (trunc `|x^-1|) => //=; rewrite in_itv/= -ltr_norml ltNge.
+apply/negP; rewrite negbK.
+by rewrite invf_ple ?posrE// ?normr_gt0// -normfV ltW// truncnS_gt.
+Qed.
+
+Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0.
+Proof.
+move: perfectly_normal_space_12 perfectly_normal_space_24 perfectly_normal_space_41.
+tauto.
+Qed.
+
+Theorem Vedenissoff_open : perfectly_normal_space_Gdelta <-> perfectly_normal_space' 0.
+Proof.
+move: Vedenissoff_closed perfectly_normal_space_23 perfectly_normal_space_32.
+tauto.
+Qed.
+
+Theorem Vedenissoff01 : perfectly_normal_space_Gdelta <-> perfectly_normal_space01.
+Proof.
+move: perfectly_normal_space_12 perfectly_normal_space_24 perfectly_normal_space_41.
+tauto.
+Qed.
+
+End perfectlynormalspace.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -95,6 +95,22 @@ Proof. by rewrite funeqE => x /=; rewrite addr0. Qed.
 Lemma center0 : center 0 = id.
 Proof. by rewrite oppr0 shift0. Qed.
 
+Lemma centerN (x y : R) : center x (- y) = - shift x y.
+Proof. by rewrite /shift opprD. Qed.
+
+Lemma shiftN (x y : R) : shift x (- y) = - center x y.
+Proof. by rewrite /shift opprD opprK. Qed.
+
+Lemma image_centerN (E : set R) (x : R) :
+  [set center x (- y) | y in E] =[set - (shift x y) | y in E].
+Proof.
+by apply/seteqP; split => y [] u Eu <- /=; exists u => //; rewrite opprD.
+Qed.
+
+Lemma image_shiftN (E : set R) (x : R) :
+  [set shift x (- y) | y in E] = [set - (center x y) | y in E].
+Proof. by rewrite -(opprK x) image_centerN opprK. Qed.
+
 End Shift.
 Arguments shift {R} x / y.
 Notation center c := (shift (- c)).