From 9f857a5a543c53fb94125f489cdbd593c0aaafdf Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 14:03:30 +0200 Subject: [PATCH 1/3] Topology lemmas --- theories/topology_theory/function_spaces.v | 5 ++ theories/topology_theory/metric_structure.v | 27 ----------- theories/topology_theory/nat_topology.v | 12 +++++ theories/topology_theory/num_topology.v | 54 +++++++++++++++++++++ 4 files changed, 71 insertions(+), 27 deletions(-) diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 9d01bf5b3b..7756614457 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -1598,6 +1598,11 @@ 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 : I), P i -> {within A, continuous (F i)}) -> + {within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}. +Proof. by move=> cont_F x; apply: 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..34febb32ff 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -93,6 +93,18 @@ 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. +Lemma near_infty_after (P : set nat) : + (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n). +Proof. +split. +- move=> [N _ afterN]. + exists N => // n /= /[swap] n' /leq_trans /[apply]. + exact: afterN. +- move=> [N _ afterN]. + exists N => // n /=. + by apply: afterN => /=. +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..a269bd3b51 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -241,6 +241,50 @@ 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 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 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_gt_y. + apply: br_sub => /=. + + by rewrite (addrC y) addrKA. + + by rewrite ltrD2r. +- move=> [/= r r0 br_sub]. + exists r => // y bxay xDa_gt_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 +296,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. +near=> t => xlt xgt. +by case/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. From bfda0759d6676802d86765c72430dfe91c321ae4 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 14:10:18 +0200 Subject: [PATCH 2/3] Update changelog --- CHANGELOG_UNRELEASED.md | 129 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9fb57d4ec6..e0f92ddec0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -11,8 +11,137 @@ + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0` + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0` +- in file `function_spaces.v`, + + new lemma `within_continuous_big`. +- in file `nat_topology.v`, + + new lemma `near_infty_after`. +- in file `num_topology.v`, + + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, and `at_right_shift`. + ### Changed +- in `realsum.v`: + + lemma `__admitted__psumB` proved and renamed to `psumB` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `topology_structure.v` to `filter.v`: + + lemma `continuous_comp` (and generalized) + +- in `numfun.v`: + + `fune_abse` renamed to `funeposDneg` and direction of the equality changed + + `funeposneg` renamed to `funeposBneg` and direction of the equality changed + + `funeD_posD` renamed to `funeDB` and direction of the equality changed + +- in `constructive_ereal.v`: + + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s + +- moved from `charge.v` to `signed_measure.v`: + + mixin `isAdditiveCharge`, structure `AdditiveCharge` + + mixin `isSemiSigmaAdditive`, structure `Charge` + + factory `isCharge` + + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, + `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` + + definitions `measure_of_charge`, `charge_of_finite_measure` + + lemma `chargeD` + + definitions `crestr`, `crestr0`, `czero`, `cscale` + + lemmas `dominates_cscalel`, `dominates_cscaler` + + definition `copp` + + lemma `cscaleN1` + + definition `cadd` + + lemmas `dominates_cadd`, `dominates_pushforward` + + definitions `positive_set`, `negative_set` + + lemmas `negative_set_charge_le0`, `negative_set0`, + `positive_negative0`, `bigcup_negative_set`, `negative_setU`, + `hahn_decomposition_lemma` + + definition `hahn_decomposition` + + theorem `Hahn_decomposition` + + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` + + definitions `jordan_pos`, `jordan_neg` + + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, + `jordan_neg_dominates` + + definition `charge_variation`, `charge_dominates` + + lemmas `abse_charge_variation`, `null_charge_dominatesP`, + `content_charge_dominatesP`, `charge_variation_continuous` + +- moved from `charge.v` to `radon_nikodym.v`: + + definition `induced_charge` + + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, + `integral_normr_continuous` + + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` + + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, + `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, + `chain_rule` + + definition `Radon_Nikodym` + + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, + `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, + `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` +- in `realsum.v`: + + the following now use `funrpos` and `funrneg`: + * definition `sum` + * lemmas `summable_funrpos`, `summable_funrneg` + + lemma `sum0` (now uses `cst`) + +- moved from `realsum` to `numfun.v`: + + now use `funrpos` and `funrneg`: + * lemmas `eq_funrpos`, `eq_funrneg` + * lemma `fpos0` (renamed to `funrpos_cst0`) + * lemma `fneg0` (renamed to `funrneg_cst0`) + * lemmas `funrposZ`, `funrnegZ` + * lemmas `funrpos_natrM`, `funrneg_natrM` + * lemmas `le_funrpos_norm` + +- moved from `numfun.v` to `unstable.v`: + + notations `nondecreasing_fun`, `nonincreasing_fun`, + `decreasing_fun`, `increasing_fun` + +- in `esum.v`: + + definition `esum` + + lemma `esum_fset` + + lemma `esum_ge` -> `PosEsum.pos_esum_ge` + + lemma `le_esum` -> `PosEsum.le_pos_esum` + +- moved from `normed_module.v` to `metric_structure.v` + + lemma `squeeze_cvgr` + +- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` + + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` + + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` +- in `normal_distribution.v: + + `normal_fun_center` -> `normal_fun_center0` + +- moved from `measurable_structure.v` to `measure_function.v`: + + definition `subset_sigma_subadditive` + +- moved from `measurable_structure.v` to `unstable.v`: + + notations `nondecreasing_seq`, `nonincreasing_seq` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + notation `^nat` + + defintion `sequence` + + defintion `seqDU` + + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` + + definition `seqD` + + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` + +- in `functions.v` + + lemma `fctE` (include `zerofctE` and `onefctE`) + +- in `classical_sets.v` + + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) + +- moved from `metric_structure.v` to `num_topology.v`: + + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. + ### Renamed ### Generalized From 7dca466ebb4fb19c2aba43993a4a999f1a856231 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 5 Aug 2026 15:36:06 +0900 Subject: [PATCH 3/3] rebase, changelog, nitpicks --- CHANGELOG_UNRELEASED.md | 132 ++--------------- theories/topology_theory/function_spaces.v | 13 +- theories/topology_theory/nat_topology.v | 23 ++- theories/topology_theory/num_topology.v | 160 +++++++++++---------- 4 files changed, 107 insertions(+), 221 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e0f92ddec0..0dac208948 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -11,133 +11,17 @@ + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0` + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0` -- in file `function_spaces.v`, - + new lemma `within_continuous_big`. -- in file `nat_topology.v`, - + new lemma `near_infty_after`. -- in file `num_topology.v`, - + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, and `at_right_shift`. +- in `function_spaces.v`: + + lemma `within_continuous_big` -### Changed - -- in `realsum.v`: - + lemma `__admitted__psumB` proved and renamed to `psumB` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `topology_structure.v` to `filter.v`: - + lemma `continuous_comp` (and generalized) - -- in `numfun.v`: - + `fune_abse` renamed to `funeposDneg` and direction of the equality changed - + `funeposneg` renamed to `funeposBneg` and direction of the equality changed - + `funeD_posD` renamed to `funeDB` and direction of the equality changed - -- in `constructive_ereal.v`: - + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s - -- moved from `charge.v` to `signed_measure.v`: - + mixin `isAdditiveCharge`, structure `AdditiveCharge` - + mixin `isSemiSigmaAdditive`, structure `Charge` - + factory `isCharge` - + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, - `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` - + definitions `measure_of_charge`, `charge_of_finite_measure` - + lemma `chargeD` - + definitions `crestr`, `crestr0`, `czero`, `cscale` - + lemmas `dominates_cscalel`, `dominates_cscaler` - + definition `copp` - + lemma `cscaleN1` - + definition `cadd` - + lemmas `dominates_cadd`, `dominates_pushforward` - + definitions `positive_set`, `negative_set` - + lemmas `negative_set_charge_le0`, `negative_set0`, - `positive_negative0`, `bigcup_negative_set`, `negative_setU`, - `hahn_decomposition_lemma` - + definition `hahn_decomposition` - + theorem `Hahn_decomposition` - + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` - + definitions `jordan_pos`, `jordan_neg` - + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, - `jordan_neg_dominates` - + definition `charge_variation`, `charge_dominates` - + lemmas `abse_charge_variation`, `null_charge_dominatesP`, - `content_charge_dominatesP`, `charge_variation_continuous` - -- moved from `charge.v` to `radon_nikodym.v`: - + definition `induced_charge` - + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, - `integral_normr_continuous` - + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` - + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, - `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, - `chain_rule` - + definition `Radon_Nikodym` - + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, - `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, - `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` -- in `realsum.v`: - + the following now use `funrpos` and `funrneg`: - * definition `sum` - * lemmas `summable_funrpos`, `summable_funrneg` - + lemma `sum0` (now uses `cst`) - -- moved from `realsum` to `numfun.v`: - + now use `funrpos` and `funrneg`: - * lemmas `eq_funrpos`, `eq_funrneg` - * lemma `fpos0` (renamed to `funrpos_cst0`) - * lemma `fneg0` (renamed to `funrneg_cst0`) - * lemmas `funrposZ`, `funrnegZ` - * lemmas `funrpos_natrM`, `funrneg_natrM` - * lemmas `le_funrpos_norm` +- in `nat_topology.v`: + + lemma `near_infty_leq` -- moved from `numfun.v` to `unstable.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, - `decreasing_fun`, `increasing_fun` +- in `num_topology.v`: + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` -- in `esum.v`: - + definition `esum` - + lemma `esum_fset` - + lemma `esum_ge` -> `PosEsum.pos_esum_ge` - + lemma `le_esum` -> `PosEsum.le_pos_esum` - -- moved from `normed_module.v` to `metric_structure.v` - + lemma `squeeze_cvgr` - -- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` - + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` - + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` -- in `normal_distribution.v: - + `normal_fun_center` -> `normal_fun_center0` - -- moved from `measurable_structure.v` to `measure_function.v`: - + definition `subset_sigma_subadditive` - -- moved from `measurable_structure.v` to `unstable.v`: - + notations `nondecreasing_seq`, `nonincreasing_seq` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + notation `^nat` - + defintion `sequence` - + defintion `seqDU` - + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` - + definition `seqD` - + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` - -- in `functions.v` - + lemma `fctE` (include `zerofctE` and `onefctE`) - -- in `classical_sets.v` - + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) +### Changed - moved from `metric_structure.v` to `num_topology.v`: + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 7756614457..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,10 +1598,11 @@ 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 : I), P i -> {within A, continuous (F i)}) -> - {within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}. -Proof. by move=> cont_F x; apply: continuous_big. 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. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 34febb32ff..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,20 +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_after (P : set nat) : - (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n). +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. -- move=> [N _ afterN]. - exists N => // n /= /[swap] n' /leq_trans /[apply]. - exact: afterN. -- move=> [N _ afterN]. - exists N => // n /=. - by apply: afterN => /=. -Qed. +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 a269bd3b51..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). @@ -244,9 +308,9 @@ 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 br_sub]. +- move=> [/= r r0 xarP]. exists r => // y bxy x_lt_y. - apply: br_sub => /=. + apply: xarP => /=. + by rewrite (addrC y) addrKA. + by rewrite ltrD2r. - move=> [/= r r0 br_sub]. @@ -261,28 +325,32 @@ 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_gt_y. + 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_gt_y. + 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)). +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)). +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^'-]). +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^'+]). +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. @@ -296,14 +364,14 @@ 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) : +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. -near=> t => xlt xgt. -by case/lt_total/orP. +by near=> t => xlt xgt /lt_total/orP[|]. Unshelve. all: by end_near. Qed. Lemma left_right_continuousP {R : realFieldType} {T : topologicalType} @@ -368,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}.