adjacent sets, cut, limit point

CHANGELOG_UNRELEASED.md

@@ -13,6 +13,13 @@
 - in `normed_module.v`:
   + lemma `limit_point_infinite_setP`
 
+- in `sequences.v`:
+  + lemma `increasing_seq_injective`
+  + definition `adjacent_set`
+  + lemmas `adjacent_sup_inf`, `adjacent_sup_inf_unique`
+  + definition `cut`
+  + lemmas `cut_adjacent`, `infinite_bounded_limit_point_nonempty`
+
 ### Changed
 
 ### Renamed

_CoqProject

@@ -84,8 +84,8 @@ theories/normedtype_theory/urysohn.v
 theories/normedtype_theory/vitali_lemma.v
 theories/normedtype_theory/normedtype.v
 
-theories/realfun.v
 theories/sequences.v
+theories/realfun.v
 theories/exp.v
 theories/trigo.v
 theories/esum.v

theories/sequences.v

@@ -2,8 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp Require Import interval archimedean.
-From mathcomp Require Import boolp classical_sets.
-From mathcomp Require Import functions set_interval reals interval_inference.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality set_interval reals interval_inference.
 From mathcomp Require Import ereal topology tvs normedtype landau.
 
 (**md**************************************************************************)
@@ -93,6 +93,12 @@ From mathcomp Require Import ereal topology tvs normedtype landau.
 (*                           of extended reals                                *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*       adjacent_set L R == L and R are two adjacent sets of real numbers    *)
+(*                cut L R == L and R are two sets of real numbers that form   *)
+(*                           a cut                                            *)
+(* ```                                                                        *)
+(*                                                                            *)
 (* ## Bounded functions                                                       *)
 (* This section proves Baire's Theorem, stating that complete normed spaces   *)
 (* are Baire spaces, and Banach-Steinhaus' theorem, stating that between a    *)
@@ -202,6 +208,20 @@ split; first by move=> u_nondec; apply: le_mono; apply: homo_ltn lt_trans _.
 by move=> u_incr n; rewrite lt_neqAle eq_le !u_incr leqnSn ltnn.
 Qed.
 
+Lemma increasing_seq_injective d {T : orderType d} (f : T^nat) :
+  increasing_seq f -> injective f.
+Proof.
+move=> incrf a b fafb; apply: contrapT => /eqP; rewrite neq_lt => /orP[ab|ba].
+- have : (f a < f b)%O.
+    rewrite (@lt_le_trans _ _ (f a.+1))//.
+      by move/increasing_seqP : incrf; exact.
+    by move: ab; rewrite incrf.
+  by rewrite fafb ltxx.
+- have := incrf a b.
+  rewrite fafb lexx => /esym.
+  by rewrite -leEnat leNgt ba.
+Qed.
+
 Lemma decreasing_seqP d (T : porderType d) (u_ : T ^nat) :
   (forall n, u_ n > u_ n.+1)%O <-> decreasing_seq u_.
 Proof.
@@ -2653,6 +2673,136 @@ apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series.
 by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0.
 Qed.
 
+Section adjacent_cut.
+Context {K : realType}.
+Implicit Types L D E : set K.
+
+Definition adjacent_set L R :=
+  [/\ L !=set0, R !=set0, (forall x y, L x -> R y -> x <= y) &
+    forall e : {posnum K}, exists2 xy, xy \in L `*` R & xy.2 - xy.1 < e%:num].
+
+Lemma adjacent_sup_inf L R : adjacent_set L R -> sup L = inf R.
+Proof.
+case=> L0 R0 LR_le LR_eps; apply/eqP; rewrite eq_le; apply/andP; split.
+  by apply: ge_sup => // x Lx; apply: lb_le_inf => // y Ry; exact: LR_le.
+apply/ler_addgt0Pl => _ /posnumP[e]; rewrite -lerBlDr.
+have [[x y]/=] := LR_eps e.
+rewrite !inE => -[/= Lx Ry] /ltW yxe.
+rewrite (le_trans _ yxe)// lerB//.
+- by rewrite ge_inf//; exists x => // z; exact: LR_le.
+- by rewrite ub_le_sup//; exists y => // z Lz; exact: LR_le.
+Qed.
+
+Lemma adjacent_sup_inf_unique L R M : adjacent_set L R ->
+  ubound L M -> lbound R M -> M = sup L.
+Proof.
+move=> [L0 R0 LR_leq LR_eps] LM RM.
+apply/eqP; rewrite eq_le ge_sup// andbT (@adjacent_sup_inf L R)//.
+exact: lb_le_inf.
+Qed.
+
+Definition cut L R := [/\ L !=set0, R !=set0,
+  (forall x y, L x -> R y -> x < y) & L `|` R = [set: K] ].
+
+Lemma cut_adjacent L R : cut L R -> adjacent_set L R.
+Proof.
+move=> [L0 R0 LRlt LRT]; split => //; first by move=> x y Lx Ry; exact/ltW/LRlt.
+move: L0 R0 => [a aL] [b bR] e.
+have ba0 : b - a > 0 by rewrite subr_gt0 LRlt.
+have [N N0 baNe] : exists2 N, N != 0 & (b - a) / N%:R < e%:num.
+  exists (truncn ((b - a) / e%:num)).+1 => //.
+  by rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// truncnS_gt.
+pose a_ i := a + i%:R * (b - a) / N%:R.
+pose k : nat := [arg min_(i < @ord_max N | a_ i \in R) i].
+have ? : a_ (@ord_max N) \in R.
+  rewrite /a_ /= mulrAC divff ?pnatr_eq0// mul1r subrKC.
+  exact/mem_set.
+have k_gt0 : (0 < k)%N.
+  rewrite /k; case: arg_minnP => // /= i aiR aRi.
+  rewrite lt0n; apply/eqP => i0.
+  move: aiR; rewrite i0 /a_ !mul0r addr0 => /set_mem.
+  by move/(LRlt _ _ aL); rewrite ltxx.
+have akN1L : a_ k.-1 \in L.
+  rewrite /k; case: arg_minnP => // /= i aiR aRi.
+  have i0 : i != ord0.
+    apply/eqP => /= i0.
+    move: aiR; rewrite /a_ i0 !mul0r addr0 => /set_mem.
+    by move/(LRlt _ _ aL); rewrite ltxx.
+  apply/mem_set; apply/notP => abs.
+  have {}abs : a_ i.-1 \in R.
+    move/seteqP : LRT => [_ /(_ (a_ i.-1) Logic.I)].
+    by case=> // /mem_set.
+  have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW.
+  have := aRi (Ordinal iN) abs.
+  apply/negP; rewrite -ltnNge/=.
+  by case: i => -[//|? ?] in i0 iN abs aiR aRi *.
+have akR : a_ k \in R by rewrite /k; case: arg_minnP => // /= i aiR aRi.
+exists (a_ k.-1, a_ k).
+  by rewrite !inE; split => //=; exact/set_mem.
+rewrite /a_ opprD addrACA subrr add0r -!mulrA -!mulrBl.
+by rewrite -natrB ?leq_pred// -subn1 subKn// mul1r.
+Qed.
+
+Lemma infinite_bounded_limit_point_nonempty E :
+  infinite_set E -> bounded_set E -> limit_point E !=set0.
+Proof.
+move=> infiniteE boundedE.
+have E0 : E !=set0.
+  apply/set0P/negP => /eqP E0.
+  by move: infiniteE; rewrite E0; apply; exact: finite_set0.
+have ? : ProperFilter (globally E).
+  by case: E0 => x Ex; exact: globally_properfilter Ex.
+pose L := [set x | infinite_set (`[x, +oo[ `&` E)].
+have L0 : L !=set0.
+  move/ex_bound : boundedE => [M EM]; exists (- M).
+  rewrite /L /= setIidr// => x Ex /=.
+  by rewrite in_itv/= andbT lerNnormlW// EM.
+pose R := ~` L.
+have R0 : R !=set0.
+  move/ex_bound : boundedE => [M EM]; exists (M + 1).
+  rewrite /R /L /= (_ : _ `&` _ = set0)// -subset0 => x []/=.
+  rewrite in_itv/= andbT => /[swap] /EM/= /ler_normlW xM.
+  by move/le_trans => /(_ _ xM); rewrite leNgt ltrDl ltr01.
+have Lle_closed x y : L x -> y <= x -> L y.
+  rewrite /L /= => xE yx.
+  rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//.
+  by apply: contra_not xE; rewrite setIUl finite_setU => -[].
+have LRlt x y : L x -> R y -> x < y.
+  by move=> Lx Ry; rewrite ltNge; apply/negP => /(Lle_closed _ _ Lx).
+have LR : cut L R by split => //; rewrite /R setUv.
+pose l := sup L. (* the real number defined by the cut (L, R) *)
+have infleE (e : K) (e0 : e > 0) :infinite_set (`]l - e, +oo[ `&` E).
+  suff : L (l - e).
+    apply: contra_not => leE.
+    rewrite -setU1itv// setIUl finite_setU; split => //.
+    by apply/(sub_finite_set _ (finite_set1 (l - e))); exact: subIsetl.
+  have : has_sup L.
+    by split => //; case: R0 => d dR; exists d => z Lz; exact/ltW/LRlt.
+  move/(sup_adherent e0) => [r Lr].
+  by rewrite -/l => /ltW ler; exact: (Lle_closed _ _ Lr).
+have finleE (e : K) (e0 : e > 0) : finite_set (`[l + e, +oo[ `&` E).
+  suff : R (l + e) by rewrite /R/= /L/= => /contrapT.
+  have : has_inf R.
+    by split => //; case: L0 => g gL; exists g => z Rz; exact/ltW/LRlt.
+  move/(inf_adherent e0) => [r Rr].
+  rewrite -(adjacent_sup_inf (cut_adjacent LR)) -/l => /ltW rle Lle.
+  have /LRlt := Lle_closed _ _ Lle rle.
+  by move/(_ _ Rr); rewrite ltxx.
+exists l; apply/limit_point_infinite_setP => /= U.
+rewrite /nbhs/= /nbhs_ball_/= => -[e /= e0].
+rewrite -[ball_ _ _ _]/(ball _ _) => leU.
+have : infinite_set (`]l - e, l + e[ `&` E).
+  rewrite (_ : _ `&` _ =
+      `]l - e, +oo[ `&` E `\` `[l + e, +oo[ `&` E); last first.
+    rewrite setDE setCI setIUr -(setIA _ _ (~` E)) setICr setI0 setU0.
+    by rewrite setIAC -setDE [in LHS]set_itv_splitD.
+  by apply: infinite_setD; [exact: infleE|exact: finleE].
+apply/contra_not/sub_finite_set; apply: setSI.
+by move: leU; rewrite ball_itv.
+Qed.
+
+End adjacent_cut.
+
 Section banach_contraction.
 
 Context {R : realType} {X : completeNormedModType R} (U : set X).