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..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 boolp classical_sets. -From mathcomp Require Import functions 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**************************************************************************) @@ -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,133 @@ 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 L D E : set R. + +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 A B : adjacent_set A B -> sup A = inf B. +Proof. +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]/=] := AB_eps e. +rewrite !inE => -[/= Ax By] /ltW yxe. +rewrite (le_trans _ yxe)// lerB//. +- 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 A B M : adjacent_set A B -> + ubound A M -> lbound B M -> M = sup A. +Proof. +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 B := [/\ L !=set0, B !=set0, + (forall x y, L x -> B y -> x < y) & L `|` B = [set: R] ]. + +Lemma cut_adjacent A B : cut A B -> adjacent_set A B. +Proof. +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 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 + 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. + 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. + have := aBi (Ordinal iN) abs. + apply/negP; rewrite -ltnNge/=. + 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. + +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 A := [set x | infinite_set (`[x, +oo[ `&` E)]. +have A0 : A !=set0. + move/ex_bound : boundedE => [M EM]; exists (- M). + rewrite /A /= setIidr// => x Ex /=. + by rewrite in_itv/= andbT lerNnormlW// EM. +pose B := ~` A. +have B0 : B !=set0. + move/ex_bound : boundedE => [M EM]; exists (M + 1). + 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 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 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 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. +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).