From 9bc260edd1ea7a35b4df22f35ec908b1d38642f4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 22 Nov 2025 00:45:11 +0900 Subject: [PATCH 1/5] adjacent sets, cut, limit point --- CHANGELOG_UNRELEASED.md | 7 ++ _CoqProject | 2 +- theories/sequences.v | 148 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 154 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 23b4ca1b57..97d3adb6ef 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/_CoqProject b/_CoqProject index 4a35dbab15..77d10c4a47 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/sequences.v b/theories/sequences.v index 780ce1e869..c48267da6f 100644 --- a/theories/sequences.v +++ b/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**************************************************************************) @@ -202,6 +202,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 +2667,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 {R : realType}. +Implicit Types G D E : set R. + +Definition adjacent_set G D := + [/\ G !=set0, D !=set0, (forall x y, G x -> D y -> x <= y) & + forall e : {posnum R}, exists2 xy, xy \in G `*` D & xy.2 - xy.1 < e%:num]. + +Lemma adjacent_sup_inf G D : adjacent_set G D -> sup G = inf D. +Proof. +case=> G0 D0 GD_le GD_eps; apply/eqP; rewrite eq_le; apply/andP; split. + by apply: ge_sup => // x Gx; apply: lb_le_inf => // y Dy; exact: GD_le. +apply/ler_addgt0Pl => _ /posnumP[e]; rewrite -lerBlDr. +have [[x y]/=] := GD_eps e. +rewrite !inE => -[/= Gx Dy] /ltW yxe. +rewrite (le_trans _ yxe)// lerB//. +- by rewrite ge_inf//; exists x => // z; exact: GD_le. +- by rewrite ub_le_sup//; exists y => // z Gz; exact: GD_le. +Qed. + +Lemma adjacent_sup_inf_unique G D M : adjacent_set G D -> + ubound G M -> lbound D M -> M = sup G. +Proof. +move=> [G0 D0 GD_leq GD_eps] GM DM. +apply/eqP; rewrite eq_le ge_sup// andbT (@adjacent_sup_inf G D)//. +exact: lb_le_inf. +Qed. + +Definition cut G D := [/\ G !=set0, D !=set0, + (forall x y, G x -> D y -> x < y) & G `|` D = [set: R] ]. + +Lemma cut_adjacent G D : cut G D -> adjacent_set G D. +Proof. +move=> [G0 D0 GDlt GDT]; split => //; first by move=> x y Gx Dy; exact/ltW/GDlt. +move: G0 D0 => [a aG] [b bD] e. +have ba0 : b - a > 0 by rewrite subr_gt0 GDlt. +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 D) i]. +have ? : a_ (@ord_max N) \in D. + rewrite /a_ /= mulrAC divff ?pnatr_eq0// mul1r subrKC. + exact/mem_set. +have k_gt0 : (0 < k)%N. + rewrite /k; case: arg_minnP => // /= i aiD aDi. + rewrite lt0n; apply/eqP => i0. + move: aiD; rewrite i0 /a_ !mul0r addr0 => /set_mem. + by move/(GDlt _ _ aG); rewrite ltxx. +have akN1G : a_ k.-1 \in G. + rewrite /k; case: arg_minnP => // /= i aiD aDi. + have i0 : i != ord0. + apply/eqP => /= i0. + move: aiD; rewrite /a_ i0 !mul0r addr0 => /set_mem. + by move/(GDlt _ _ aG); rewrite ltxx. + apply/mem_set; apply/notP => abs. + have {}abs : a_ i.-1 \in D. + move/seteqP : GDT => [_ /(_ (a_ i.-1) Logic.I)]. + by case=> // /mem_set. + have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW. + have := aDi (Ordinal iN) abs. + apply/negP; rewrite -ltnNge/=. + by case: i => -[//|? ?] in i0 iN abs aiD aDi *. +have akD : a_ k \in D by rewrite /k; case: arg_minnP => // /= i aiD aDi. +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 G := [set x | infinite_set (`[x, +oo[ `&` E)]. +have G0 : G !=set0. + move/ex_bound : boundedE => [M EM]; exists (- M). + rewrite /G /= setIidr// => x Ex /=. + by rewrite in_itv/= andbT lerNnormlW// EM. +pose D := ~` G. +have D0 : D !=set0. + move/ex_bound : boundedE => [M EM]; exists (M + 1). + rewrite /D /G /= (_ : _ `&` _ = set0)// -subset0 => x []/=. + rewrite in_itv/= andbT => /[swap] /EM/= /ler_normlW xM. + by move/le_trans => /(_ _ xM); rewrite leNgt ltrDl ltr01. +have Gle_closed x y : G x -> y <= x -> G y. + rewrite /G /= => xE yx. + rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//. + by apply: contra_not xE; rewrite setIUl finite_setU => -[]. +have GDlt x y : G x -> D y -> x < y. + by move=> Gx Dy; rewrite ltNge; apply/negP => /(Gle_closed _ _ Gx). +have GD : cut G D by split => //; rewrite /D setUv. +pose l := sup G. (* the real number defined by the cut (G, D) *) +have infleE (e : R) (e0 : e > 0) :infinite_set (`]l - e, +oo[ `&` E). + suff : G (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 G. + by split => //; case: D0 => d dD; exists d => z Gz; exact/ltW/GDlt. + move/(sup_adherent e0) => [r Gr]. + by rewrite -/l => /ltW K; exact: (Gle_closed _ _ Gr). +have finleE (e : R) (e0 : e > 0) : finite_set (`[l + e, +oo[ `&` E). + suff : D (l + e) by rewrite /D/= /G/= => /contrapT. + have : has_inf D. + by split => //; case: G0 => g gG; exists g => z Dz; exact/ltW/GDlt. + move/(inf_adherent e0) => [r Dr]. + rewrite -(adjacent_sup_inf (cut_adjacent GD)) -/l => /ltW rle Gle. + have /GDlt := Gle_closed _ _ Gle rle. + by move/(_ _ Dr); 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). From ccd3587775a3eb9ccff6f1af9413a23226a27935 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 22 Nov 2025 00:52:52 +0900 Subject: [PATCH 2/5] doc --- theories/sequences.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/theories/sequences.v b/theories/sequences.v index c48267da6f..5d47c178fa 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -93,6 +93,12 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* of extended reals *) (* ``` *) (* *) +(* ``` *) +(* adjacent_set G D == G and D are two adjacent sets of real numbers *) +(* cut G D == G and D 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 *) From 6a3de7455efb84d72958b3d2aa63c59268727c50 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 11:04:06 +0900 Subject: [PATCH 3/5] D->R, G->L --- theories/sequences.v | 128 +++++++++++++++++++++---------------------- 1 file changed, 64 insertions(+), 64 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 5d47c178fa..04f9ce0bb2 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -94,8 +94,8 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* ``` *) (* *) (* ``` *) -(* adjacent_set G D == G and D are two adjacent sets of real numbers *) -(* cut G D == G and D are two sets of real numbers that form *) +(* 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 *) (* ``` *) (* *) @@ -2674,69 +2674,69 @@ by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. Qed. Section adjacent_cut. -Context {R : realType}. -Implicit Types G D E : set R. +Context {K : realType}. +Implicit Types L D E : set K. -Definition adjacent_set G D := - [/\ G !=set0, D !=set0, (forall x y, G x -> D y -> x <= y) & - forall e : {posnum R}, exists2 xy, xy \in G `*` D & xy.2 - xy.1 < e%:num]. +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 G D : adjacent_set G D -> sup G = inf D. +Lemma adjacent_sup_inf L R : adjacent_set L R -> sup L = inf R. Proof. -case=> G0 D0 GD_le GD_eps; apply/eqP; rewrite eq_le; apply/andP; split. - by apply: ge_sup => // x Gx; apply: lb_le_inf => // y Dy; exact: GD_le. +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]/=] := GD_eps e. -rewrite !inE => -[/= Gx Dy] /ltW yxe. +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: GD_le. -- by rewrite ub_le_sup//; exists y => // z Gz; exact: GD_le. +- 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 G D M : adjacent_set G D -> - ubound G M -> lbound D M -> M = sup G. +Lemma adjacent_sup_inf_unique L R M : adjacent_set L R -> + ubound L M -> lbound R M -> M = sup L. Proof. -move=> [G0 D0 GD_leq GD_eps] GM DM. -apply/eqP; rewrite eq_le ge_sup// andbT (@adjacent_sup_inf G D)//. +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 G D := [/\ G !=set0, D !=set0, - (forall x y, G x -> D y -> x < y) & G `|` D = [set: R] ]. +Definition cut L R := [/\ L !=set0, R !=set0, + (forall x y, L x -> R y -> x < y) & L `|` R = [set: K] ]. -Lemma cut_adjacent G D : cut G D -> adjacent_set G D. +Lemma cut_adjacent L R : cut L R -> adjacent_set L R. Proof. -move=> [G0 D0 GDlt GDT]; split => //; first by move=> x y Gx Dy; exact/ltW/GDlt. -move: G0 D0 => [a aG] [b bD] e. -have ba0 : b - a > 0 by rewrite subr_gt0 GDlt. +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 D) i]. -have ? : a_ (@ord_max N) \in D. +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 aiD aDi. + rewrite /k; case: arg_minnP => // /= i aiR aRi. rewrite lt0n; apply/eqP => i0. - move: aiD; rewrite i0 /a_ !mul0r addr0 => /set_mem. - by move/(GDlt _ _ aG); rewrite ltxx. -have akN1G : a_ k.-1 \in G. - rewrite /k; case: arg_minnP => // /= i aiD aDi. + 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: aiD; rewrite /a_ i0 !mul0r addr0 => /set_mem. - by move/(GDlt _ _ aG); rewrite ltxx. + 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 D. - move/seteqP : GDT => [_ /(_ (a_ i.-1) Logic.I)]. + 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 := aDi (Ordinal iN) abs. + have := aRi (Ordinal iN) abs. apply/negP; rewrite -ltnNge/=. - by case: i => -[//|? ?] in i0 iN abs aiD aDi *. -have akD : a_ k \in D by rewrite /k; case: arg_minnP => // /= i aiD aDi. + 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. @@ -2752,42 +2752,42 @@ have E0 : E !=set0. by move: infiniteE; rewrite E0; apply; exact: finite_set0. have ? : ProperFilter (globally E). by case: E0 => x Ex; exact: globally_properfilter Ex. -pose G := [set x | infinite_set (`[x, +oo[ `&` E)]. -have G0 : G !=set0. +pose L := [set x | infinite_set (`[x, +oo[ `&` E)]. +have L0 : L !=set0. move/ex_bound : boundedE => [M EM]; exists (- M). - rewrite /G /= setIidr// => x Ex /=. + rewrite /L /= setIidr// => x Ex /=. by rewrite in_itv/= andbT lerNnormlW// EM. -pose D := ~` G. -have D0 : D !=set0. +pose R := ~` L. +have R0 : R !=set0. move/ex_bound : boundedE => [M EM]; exists (M + 1). - rewrite /D /G /= (_ : _ `&` _ = set0)// -subset0 => x []/=. + 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 Gle_closed x y : G x -> y <= x -> G y. - rewrite /G /= => xE yx. +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 GDlt x y : G x -> D y -> x < y. - by move=> Gx Dy; rewrite ltNge; apply/negP => /(Gle_closed _ _ Gx). -have GD : cut G D by split => //; rewrite /D setUv. -pose l := sup G. (* the real number defined by the cut (G, D) *) -have infleE (e : R) (e0 : e > 0) :infinite_set (`]l - e, +oo[ `&` E). - suff : G (l - e). +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 G. - by split => //; case: D0 => d dD; exists d => z Gz; exact/ltW/GDlt. - move/(sup_adherent e0) => [r Gr]. - by rewrite -/l => /ltW K; exact: (Gle_closed _ _ Gr). -have finleE (e : R) (e0 : e > 0) : finite_set (`[l + e, +oo[ `&` E). - suff : D (l + e) by rewrite /D/= /G/= => /contrapT. - have : has_inf D. - by split => //; case: G0 => g gG; exists g => z Dz; exact/ltW/GDlt. - move/(inf_adherent e0) => [r Dr]. - rewrite -(adjacent_sup_inf (cut_adjacent GD)) -/l => /ltW rle Gle. - have /GDlt := Gle_closed _ _ Gle rle. - by move/(_ _ Dr); rewrite ltxx. + 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. From c22a680d9bad1705cdf4c6dcea352999f4cb6483 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 18:21:59 +0900 Subject: [PATCH 4/5] LR -> AB --- theories/sequences.v | 133 +++++++++++++++++++++---------------------- 1 file changed, 65 insertions(+), 68 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 04f9ce0bb2..0f5e3c2a78 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2674,71 +2674,68 @@ by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. Qed. Section adjacent_cut. -Context {K : realType}. -Implicit Types L D E : set K. +Context {R : realType}. +Implicit Types L D E : set R. -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]. +Definition adjacent_set A B := + [/\ A !=set0, B !=set0, (forall x y, A x -> B y -> x <= y) & + forall e : {posnum R}, exists2 xy, xy \in A `*` B & xy.2 - xy.1 < e%:num]. -Lemma adjacent_sup_inf L R : adjacent_set L R -> sup L = inf R. +Lemma adjacent_sup_inf A B : adjacent_set A B -> sup A = inf B. 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. +case=> A0 B0 AB_le AB_eps; apply/eqP; rewrite eq_le; apply/andP; split. + by apply: ge_sup => // x Ax; apply: lb_le_inf => // y By; exact: AB_le. apply/ler_addgt0Pl => _ /posnumP[e]; rewrite -lerBlDr. -have [[x y]/=] := LR_eps e. -rewrite !inE => -[/= Lx Ry] /ltW yxe. +have [[x y]/=] := AB_eps e. +rewrite !inE => -[/= Ax By] /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. +- by rewrite ge_inf//; exists x => // z; exact: AB_le. +- by rewrite ub_le_sup//; exists y => // z Az; exact: AB_le. Qed. -Lemma adjacent_sup_inf_unique L R M : adjacent_set L R -> - ubound L M -> lbound R M -> M = sup L. +Lemma adjacent_sup_inf_unique A B M : adjacent_set A B -> + ubound A M -> lbound B M -> M = sup A. Proof. -move=> [L0 R0 LR_leq LR_eps] LM RM. -apply/eqP; rewrite eq_le ge_sup// andbT (@adjacent_sup_inf L R)//. +move=> [A0 B0 AB_leq AB_eps] AM BM. +apply/eqP; rewrite eq_le ge_sup// andbT (@adjacent_sup_inf A B)//. 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] ]. +Definition cut L B := [/\ L !=set0, B !=set0, + (forall x y, L x -> B y -> x < y) & L `|` B = [set: R] ]. -Lemma cut_adjacent L R : cut L R -> adjacent_set L R. +Lemma cut_adjacent A B : cut A B -> adjacent_set A B. 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. +move=> [A0 B0 ABlt ABT]; split => //; first by move=> x y Ax By; exact/ltW/ABlt. +move: A0 B0 => [a aA] [b bB] e. +have ba0 : b - a > 0 by rewrite subr_gt0 ABlt. 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. +pose k : nat := [arg min_(i < @ord_max N | a_ i \in B) i]. +have ? : a_ (@ord_max N) \in B. + by 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 /k; case: arg_minnP => // /= i aiB aBi. 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. + move: aiB; rewrite i0 /a_ !mul0r addr0 => /set_mem. + by move/(ABlt _ _ aA); rewrite ltxx. +have akN1A : a_ k.-1 \in A. + rewrite /k; case: arg_minnP => // /= i aiB aBi. 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. + move: aiB; rewrite /a_ i0 !mul0r addr0 => /set_mem. + by move/(ABlt _ _ aA); rewrite ltxx. + apply/mem_set/notP => abs. + have {}abs : a_ i.-1 \in B. + by move/seteqP : ABT => [_ /(_ (a_ i.-1) Logic.I)] [//|/mem_set]. have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW. - have := aRi (Ordinal iN) abs. + have := aBi (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. + by case: i => -[//|? ?] in i0 iN abs aiB aBi *. +have akB : a_ k \in B by rewrite /k; case: arg_minnP => // /= i aiB aBi. +exists (a_ k.-1, a_ k); first by rewrite !inE; split => //=; exact/set_mem. rewrite /a_ opprD addrACA subrr add0r -!mulrA -!mulrBl. by rewrite -natrB ?leq_pred// -subn1 subKn// mul1r. Qed. @@ -2752,42 +2749,42 @@ have E0 : E !=set0. 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. +pose A := [set x | infinite_set (`[x, +oo[ `&` E)]. +have A0 : A !=set0. move/ex_bound : boundedE => [M EM]; exists (- M). - rewrite /L /= setIidr// => x Ex /=. + rewrite /A /= setIidr// => x Ex /=. by rewrite in_itv/= andbT lerNnormlW// EM. -pose R := ~` L. -have R0 : R !=set0. +pose B := ~` A. +have B0 : B !=set0. move/ex_bound : boundedE => [M EM]; exists (M + 1). - rewrite /R /L /= (_ : _ `&` _ = set0)// -subset0 => x []/=. + rewrite /B /A /= (_ : _ `&` _ = 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. +have Ale_closed x y : A x -> y <= x -> A y. + rewrite /A /= => 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). +have ABlt x y : A x -> B y -> x < y. + by move=> Ax By; rewrite ltNge; apply/negP => /(Ale_closed _ _ Ax). +have AB : cut A B by split => //; rewrite /B setUv. +pose l := sup A. (* the real number defined by the cut (A, B) *) +have infleE (e : R) (e0 : e > 0) :infinite_set (`]l - e, +oo[ `&` E). + suff : A (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. + have : has_sup A. + by split => //; case: B0 => d dB; exists d => z Az; exact/ltW/ABlt. + move/(sup_adherent e0) => [r Ar]. + by rewrite -/l => /ltW ler; exact: (Ale_closed _ _ Ar). +have finleE (e : R) (e0 : e > 0) : finite_set (`[l + e, +oo[ `&` E). + suff : B (l + e) by rewrite /B/= /A/= => /contrapT. + have : has_inf B. + by split => //; case: A0 => g gA; exists g => z Bz; exact/ltW/ABlt. + move/(inf_adherent e0) => [r Br]. + rewrite -(adjacent_sup_inf (cut_adjacent AB)) -/l => /ltW rle Ale. + have /ABlt := Ale_closed _ _ Ale rle. + by move/(_ _ Br); rewrite ltxx. exists l; apply/limit_point_infinite_setP => /= U. rewrite /nbhs/= /nbhs_ball_/= => -[e /= e0]. rewrite -[ball_ _ _ _]/(ball _ _) => leU. From dea336e29794588b54a88fd84a6e5b9348a56abf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 18:47:48 +0900 Subject: [PATCH 5/5] use contra --- theories/sequences.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 0f5e3c2a78..067000fe99 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1,9 +1,9 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint. -From mathcomp Require Import interval archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality set_interval reals interval_inference. +From mathcomp Require Import interval interval_inference archimedean. +From mathcomp Require Import mathcomp_extra boolp contra classical_sets. +From mathcomp Require Import functions cardinality set_interval reals. From mathcomp Require Import ereal topology tvs normedtype landau. (**md**************************************************************************) @@ -2717,17 +2717,17 @@ pose k : nat := [arg min_(i < @ord_max N | a_ i \in B) i]. have ? : a_ (@ord_max N) \in B. by rewrite /a_ /= mulrAC divff ?pnatr_eq0// mul1r subrKC; exact/mem_set. have k_gt0 : (0 < k)%N. - rewrite /k; case: arg_minnP => // /= i aiB aBi. - rewrite lt0n; apply/eqP => i0. - move: aiB; rewrite i0 /a_ !mul0r addr0 => /set_mem. - by move/(ABlt _ _ aA); rewrite ltxx. + rewrite /k; case: arg_minnP => // /= i + aBi. + contra; rewrite leqn0 => /eqP ->. + rewrite /a_ !mul0r addr0; apply/negP => /set_mem/(ABlt _ _ aA). + by rewrite ltxx. have akN1A : a_ k.-1 \in A. rewrite /k; case: arg_minnP => // /= i aiB aBi. have i0 : i != ord0. - apply/eqP => /= i0. - move: aiB; rewrite /a_ i0 !mul0r addr0 => /set_mem. - by move/(ABlt _ _ aA); rewrite ltxx. - apply/mem_set/notP => abs. + contra: aiB => ->. + rewrite /a_ !mul0r addr0; apply/negP => /set_mem/(ABlt _ _ aA). + by rewrite ltxx. + apply/mem_set/boolp.notP => abs. have {}abs : a_ i.-1 \in B. by move/seteqP : ABT => [_ /(_ (a_ i.-1) Logic.I)] [//|/mem_set]. have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW.