diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9fb57d4ec6..0dac208948 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -11,8 +11,21 @@ + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0` + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0` +- in `function_spaces.v`: + + lemma `within_continuous_big` + +- in `nat_topology.v`: + + lemma `near_infty_leq` + +- in `num_topology.v`: + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` + ### Changed +- moved from `metric_structure.v` to `num_topology.v`: + + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. + ### Renamed ### Generalized diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 9d01bf5b3b..420e2a22c0 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -1565,8 +1565,8 @@ End cartesian_closed. End currying. Section big_continuous. -Context {U : topologicalType} {I : Type}. -Variables (op : U -> U -> U) (x0 : U) (P : pred I). +Context {U : topologicalType} {I : Type} + (op : U -> U -> U) (x0 : U) (P : pred I). Hypothesis cont_op : continuous (fun x : U * U => op x.1 x.2). Lemma cvg_big {T : Type} (F : set_system T) (r : seq I) @@ -1598,6 +1598,12 @@ Proof. by move=> F_cont x; apply: cvg_big => // i /F_cont; exact. Qed. +Lemma within_continuous_big {T : topologicalType} (A : set T) (r : seq I) + (F : I -> T -> U) : + (forall i, P i -> {within A, continuous (F i)}) -> + {within A, continuous (fun x => \big[op/x0]_(i <- r | P i) F i x)}. +Proof. by move=> ? ?; exact: continuous_big. Qed. + End big_continuous. Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y := diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index ee6eda7fe9..85c6eacf1c 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -315,33 +315,6 @@ Unshelve. all: end_near. Qed. End cvg_nbhsP. -Section cvg_at_right_left_dnbhs. -Variables (R : realFieldType) (T : metricType R). - -Import metricType_numDomainType. - -Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) : - f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> - f x @[x --> p^'] --> l. -Proof. -move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0. -have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0. -have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0. -near=> t. -have : t != p by near: t; exact: nbhs_dnbhs_neq. -rewrite neq_lt => /orP[tp|pt]. -- apply: fpnl => //=; near: t. - exists (b / 2) => //=; first by rewrite divr_gt0. - move=> z/= + _ => /lt_le_trans; apply. - by rewrite ler_pdivrMr// ler_pMr// ler1n. -- apply: fppl =>//=; near: t. - exists (a / 2) => //=; first by rewrite divr_gt0. - move=> z/= + _ => /lt_le_trans; apply. - by rewrite ler_pdivrMr// ler_pMr// ler1n. -Unshelve. all: by end_near. Qed. - -End cvg_at_right_left_dnbhs. - Section at_left_rightR. Variable (R : numFieldType). diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index b1a7a63e36..9f2a95bf90 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order algebra all_classical. #[warning="-warn-library-file-internal-analysis"] @@ -90,8 +90,17 @@ by rewrite /= -leq_divRL//; apply: Pn. Qed. Lemma near_inftyS (P : set nat) : - (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x). -Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed. + (\forall x \near \oo, P x.+1) -> (\forall x \near \oo, P x). +Proof. by case=> N _ NPS; exists N.+1 => // [[]]; rewrite ?ltn0. Qed. + +Lemma near_infty_leq (P : set nat) : + (\forall n \near \oo, P n) <-> + (\forall N \near \oo, forall n, (n >= N)%N -> P n). +Proof. +split => [[N _ /= NP]|]. + by exists N => // n/= Nn m /(leq_trans Nn); exact: NP. +by apply: filterS => N; exact. +Qed. Section infty_nat. Local Open Scope nat_scope. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index d5078ca012..268223d570 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -13,6 +13,9 @@ From mathcomp Require Import order_topology matrix_topology. (* *) (******************************************************************************) +Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+"). +Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-"). + Import Order.TTheory GRing.Theory Num.Theory. Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) @@ -146,11 +149,72 @@ Module Exports. HB.reexport. End Exports. End numFieldTopology. Import numFieldTopology.Exports. -Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+"). -Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-"). +Lemma nbhsN {R : numFieldType} (x : R) : nbhs (- x) = -%R @ x. +Proof. +rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=. + by move=> ?; apply: xeA => //=; rewrite -opprD normrN. +by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK. +Qed. + +Lemma cvg_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) (a : R) + (l : T) : + (f \o -%R) x @[x --> a] --> l <-> f x @[x --> (- a)] --> l. +Proof. by rewrite nbhsN. Qed. + +Lemma withinN {R : numFieldType} (A : set R) (r : R) : + within A (nbhs (- r)) = - x @[x --> within (-%R @` A) (nbhs r)]. +Proof. +rewrite eqEsubset /=; split; move=> E /= [e e0 reE]; exists e => //. + move=> s rse sA; apply: reE; last by rewrite memNE opprK. + by rewrite /= opprK addrC distrC. +move=> s res rs; rewrite -(opprK s); apply: reE; last by rewrite -memNE. +by rewrite /= opprK -normrN opprD. +Qed. + +Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) : + (\forall y \near - x, P y) <-> \near x, P (- x). +Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed. + +Lemma nbhsNimage {R : numFieldType} (x : R) : + nbhs (- x) = [set -%R @` A | A in nbhs x]. +Proof. +rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr. +by rewrite (eq_imageK opprK opprK). +Qed. + +Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A]. +Proof. +move=> Aop; rewrite openE => _ [x /Aop x_A <-]. +by rewrite /interior nbhsNimage; exists A. +Qed. + +Lemma closedN (R : numFieldType) (A : set R) : + closed A -> closed [set - x | x in A]. +Proof. +move=> Acl x clNAx. +suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK. +move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0. + by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B. +move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). +by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. +Qed. + +Lemma dnbhsN {R : numFieldType} (r : R) : + (- r)%R^' = (fun A => -%R @` A) @` r^'. +Proof. +apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]]. + exists (-%R @` A). + exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//. + by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC. + rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=. + by rewrite opprK. +exists e => //= x/=; rewrite -opprD normrN => axe xa. +exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=. +by rewrite opprK. +Qed. Section at_left_right. -Variable R : numFieldType. +Context {R : numFieldType}. Definition at_left (x : R) := within (fun u => u < x) (nbhs x). Definition at_right (x : R) := within (fun u => x < u) (nbhs x). @@ -241,6 +305,54 @@ split=> [pPf e|ex_notPx]. by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl. Unshelve. all: by end_near. Qed. +Lemma at_rightD x a : (x + a)^'+ = (y + a @[y --> x^'+]). +Proof. +apply/seteqP; split=> P /=. +- move=> [/= r r0 xarP]. + exists r => // y bxy x_lt_y. + apply: xarP => /=. + + by rewrite (addrC y) addrKA. + + by rewrite ltrD2r. +- move=> [/= r r0 br_sub]. + exists r => // y bxay xDa_lt_y. + rewrite -(subrK a y). + apply: br_sub => /=. + + by rewrite opprB addrA. + + by rewrite ltrBrDr. +Qed. + +Lemma at_leftD x a : (x + a)^'- = (y + a @[y --> x^'-]). +Proof. +apply/seteqP; split=> P /=. +- move=> [/= r r0 br_sub]. + exists r => // y bxy x_lt_y. + apply: br_sub => /=. + + by rewrite (addrC y) addrKA. + + by rewrite ltrD2r. +- move=> [/= r r0 br_sub]. + exists r => // y bxay xDa_lt_y. + rewrite -(subrK a y). + apply: br_sub => /=. + + by rewrite opprB addrA. + + by rewrite ltrBlDr. +Qed. + +Lemma near_at_rightD x a (P : set R) : + (\forall y \near (x + a)^'+, P y) = (\forall y \near x^'+, P (y + a)). +Proof. by rewrite at_rightD near_map. Qed. + +Lemma near_at_leftD x a (P : set R) : + (\forall y \near (x + a)^'-, P y) = (\forall y \near x^'-, P (y + a)). +Proof. by rewrite at_leftD near_map. Qed. + +Lemma at_left_shift (T : Type) x a (f : R -> T) : + (f @ (x + a)^'-) = (f (y + a) @[y --> x^'-]). +Proof. by rewrite at_leftD. Qed. + +Lemma at_right_shift (T : Type) x a (f : R -> T) : + (f @ (x + a)^'+) = (f (y + a) @[y --> x^'+]). +Proof. by rewrite at_rightD. Qed. + End at_left_right. #[global] Typeclasses Opaque at_left at_right. Notation "x ^'-" := (at_left x) : classical_set_scope. @@ -252,6 +364,16 @@ Notation "x ^'+" := (at_right x) : classical_set_scope. #[global] Hint Extern 0 (Filter (nbhs _^'-)) => (apply: at_left_proper_filter) : typeclass_instances. +Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType) + (f : R -> T) (p : R) (l : T) : + f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l. +Proof. +move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite !near_withinE !near_nbhs => lf rf. +apply: filter_app lf; apply: filter_app rf. +by near=> t => xlt xgt /lt_total/orP[|]. +Unshelve. all: by end_near. Qed. + Lemma left_right_continuousP {R : realFieldType} {T : topologicalType} (f : R -> T) x : f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x. @@ -314,70 +436,6 @@ have : inf X <= inf X - f%:num by exact: ge_inf. by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl. Qed. -Lemma nbhsN {R : numFieldType} (x : R) : nbhs (- x) = -%R @ x. -Proof. -rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=. - by move=> ?; apply: xeA => //=; rewrite -opprD normrN. -by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK. -Qed. - -Lemma cvg_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) (a : R) - (l : T) : - (f \o -%R) x @[x --> a] --> l <-> f x @[x --> (- a)] --> l. -Proof. by rewrite nbhsN. Qed. - -Lemma nbhsNimage {R : numFieldType} (x : R) : - nbhs (- x) = [set -%R @` A | A in nbhs x]. -Proof. -rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr. -by rewrite (eq_imageK opprK opprK). -Qed. - -Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) : - (\forall y \near - x, P y) <-> \near x, P (- x). -Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed. - -Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A]. -Proof. -move=> Aop; rewrite openE => _ [x /Aop x_A <-]. -by rewrite /interior nbhsNimage; exists A. -Qed. - -Lemma closedN (R : numFieldType) (A : set R) : - closed A -> closed [set - x | x in A]. -Proof. -move=> Acl x clNAx. -suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK. -move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0. - by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B. -move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). -by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. -Qed. - -Lemma dnbhsN {R : numFieldType} (r : R) : - (- r)%R^' = (fun A => -%R @` A) @` r^'. -Proof. -apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]]. - exists (-%R @` A). - exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//. - by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC. - rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=. - by rewrite opprK. -exists e => //= x/=; rewrite -opprD normrN => axe xa. -exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=. -by rewrite opprK. -Qed. - -Lemma withinN {R : numFieldType} (A : set R) (r : R) : - within A (nbhs (- r)) = - x @[x --> within (-%R @` A) (nbhs r)]. -Proof. -rewrite eqEsubset /=; split; move=> E /= [e e0 reE]; exists e => //. - move=> s rse sA; apply: reE; last by rewrite memNE opprK. - by rewrite /= opprK addrC distrC. -move=> s res rs; rewrite -(opprK s); apply: reE; last by rewrite -memNE. -by rewrite /= opprK -normrN opprD. -Qed. - Lemma in_continuous_mksetP {T : realFieldType} {U : nbhsType} (i : interval T) (f : T -> U) : {in i, continuous f} <-> {in [set` i], continuous f}.