From 5da4c39549eb7385fb3464109aa4c9946c28f3ed Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 01/18] adding seminorms to tvs - adding also initial fam topology, gauge functions, and subbase 0basis - hahn banach initial_subctvs Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 214 +++++++++++++++++++++++++++++++ theories/normedtype_theory/tvs.v | 1 + 2 files changed, 215 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7f0405803..f2201b196e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,6 +9,220 @@ `pownMexpR_cvgr0`, `powRMexpR_cvgr0`, `pownMpowR_cvgr0`, `pownMexpr_cvgn0` + instance `is_derive1_powRl` +- in `ereal_normedtype.v`: + + lemma `ge0_cvgMly` +- in `unstable.v`: + + lemma `itv_boundlr_lt`, + + module `EndlessDense` + * definitions `is_endless`, `is_dense` + * lemmas `itv_bound_half_dense` + * defintions `dual_itv_bound`, `dual_itv` + * lemmas `dual_itvE`, `dual_itv_sub_memP`, `dual_is_dense`, `dual_is_endless`, + ` dual_itv_boundK`, `dual_itv_bound_lt`, `dual_itv_bound_le` + * lemmas `subitvP`, `numDomain_is_endless`, `numField_is_dense` + + lemma `real_subitvP` + +- in `classical_sets.v`: + + lemma `powerset0`, `powerset1`, `powerset2`, `powersetS`, + `setorder_itv_setUl_image`, `setorder_itv_setUr_image`, + `setorder_itv_setDl_image` + +- in set_interval.v + + lemmas `itv_open_endsPn`, `itv_closed_endsPn`, `itv_open_ends_boundlr` + +- in topology_structure.v + + lemmas `closureEbigcap_itvcy`,`interiorEbigcup_itvNyc`, + `closureEbigcap_itvcc`,`interiorEbigcup_itvcc` + +- in num_topology.v + + module `EndlessDenseTopology` (internal) + + lemmas `open_itv_open_ends`, `closed_itv_closed_ends`, + `itv_closureE`, `itv_interiorE` + +- in `sequences.v`: + + lemma `sdrop_shift` + + lemma `ge_einfs` + + lemma `einfs_shift` + + lemma `limn_einf_shift_new` + + lemma `limn_einf_shiftS` + + lemma `limn_einf_cst` +- in `uniform_structure.v`: + + lemma `unif_continuous_continuous` +- in `uniform_structure.v`: + + lemma `unif_continuous_comp` + +- in `initial_topology.v`: + + lemma `initial_unif_continuous` + + lemma `initial_unif_continuous_comp` + + lemma `initial_unif_continuous_comp_fst` + + lemma `initial_unif_continuous_comp_snd` + + lemma `initial_nbhs_preimage` + +- in `product_topology.v`: + + lemma `entourage_prod_exS` + + definition `interchange_prod` + + lemma `entourage_interchange_prod` + + lemma `pair_unif_continuous` + + lemma `fst_unif_continuous` + + lemma `snd_unif_continuous` + +- in `metric_space.v`: + + definition `prod_mdist` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `PseudoMetricNormedZmodule_add_unif_continuous` + + lemma `PseudoMetricNormedZmodule_opp_unif_continuous` + + lemma `standard_scale_continuous` + + notation `topologicalNmodType` + +- in `sequences.v`, + + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` + +- in `num_normedtype.v`, + + lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, + `lt0_cvgMrNy`, `lt0_cvgMly`, `lt0_cvgMry` + +- in `pseudometric_normed_Zmodule.v`, + + lemmas `fmap_at_left0P`, `fmap_at_right0E` + +- in `unstable.v`: + + definitions `clamp`, `clamp_gele` + + lemmas `clamp_gemin`, `clamp_lemax`, `minmax_clamp`, + `clamp_id`, `clamp_min`, `clamp_max` + + lemma `seminorm_normrB` + +- in `topology_structure.v`: + + lemma `id_continuous` + + definition `nbhs_basis` + + definition `openU_from` + +- in `normed_module.v`: + + lemma `ball_convex_set` (was a `Let`) + +- in `classical_sets.v`: + + notation ``... `+ ...`` + + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA` + +- in `convex.v`: + + lemmas `lt_conv`, `le_conv` + + lemma `convD` + +- in `pseudmetric_normed_Zmodule.v`: + + lemma `continuous_shift` + + lemma `nbhs_add1set` + +- in `tvs.v`: + + definition `balanced_set` + + definition `absolutely_convex_set` + + lemma `absolutely_convex0` + + definition `absorbing_set` + + lemma `absolutely_convex_setX` + + definition `init_subconvextvs` + + factory `NbhsBasisAt0_isConvexTvs` + + definition `filter_from_basis0` + + factory `NbhsSubbasisAt0_isConvexTvs` + + definition `finI_fromsubbasis0` + + lemma `openD` + + lemma `openB` + + lemma `nbhsE0` + + lemma `openZ` + + lemma `continuousZl` + + lemma `continuousZr` + + lemma `scalerx_continuous` + + lemma `scalexr_continuous` + + definition `nbhsbasis_convextvs` + + definition `open_nbhsbasis_convextvs` + + definition `open_absconvex_opennbhsbasis` + + definition `basis_opennbhsbasis` + + lemma `basis_neqset0` + + lemma `absorbing_opennbhsbasis` + + definition `gauge_fun` + + definition `seminorm_on` + + definition `seminorm_subbasis` + + lemmas `nonempty_subbasis`, `mem0_seminorm_subbasis`, `split_seminorm_subbasis`, + `expand_seminorm_subbasis` + + lemmas `convex_seminorm_subbasis`, `balanced_seminorm_subbasis`, + `absolutely_convex_seminorm_subbasis`, `absorbing_seminorm`, `continuous_at0_seminorm`, + `continuous_seminorm` + + definitions `gauge_fun_basis`, `seminorm_of` + + theorem `seminorm_convextvs` + + lemma `continuous_seminorm_of` + + lemma `linear_continuous_seminorm` + + lemma `linear_seminorm_continuous` + + proposition `lcfun_seminorm` + +- in `hahn_banach_theorem.v` + + theorem `hahn_banach_extension_subctvs` + + theorem `hahn_banach_extension_initialsubctvs` + +- in `sequences.v`, + + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` + +- new file `edist.v` +- in `classical_sets.v` + + lemma `bigcup_idset1` + +- in `esum.v`: + + lemma `nonempty_esumy` + + lemma `infinite_esum_cst` + +- in `random_variable.v`: + + lemma `not_range_pmf0` + + lemma `dRV_esum_pmf_distribution` + +- in `measure_theory/measure_function.v`: + + lemma `semi_cvg_measure_bigcap` +- in `num_normedtype.v`: + + `continuous_within_itvbbP`, + `continuous_within_itvocP`, `continuous_within_itvcoP`, + `continuous_within_itvbyP`, `continuous_within_itvNybP` +- in `num_topology.v`: + + lemma `not_nearP` + + lemma `not_nearPball` +- in `pseudometric_structure.v`: + + lemma `cvg_withinP` + +- in `ftc.v`: + + lemma `integration_by_partsy_ge0_ge0` + + lemma `integration_by_partsy_le0_ge0` + + lemma `integration_by_partsy_le0_le0` + + lemma `integration_by_partsy_ge0_le0` + +- in `realfun.v`: + + lemma `derivable_oy_RcontinuousN` + +- in `topology_structure.v`: + + definitions `separable_set`, `separable` + + lemmas `basisP`, `separableTE`, `second_countable_separable`, + `bigcupT_separable`, `bigcup_separable` +- 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`, `at_right_shift`, `near_right_in_itv`, and `near_left_in_itv`. +- in file `nat_topology.v`: + + lemma `near_infty_after` + +- in file `realfun.v`: + + new lemmas `lhopital_at_pinfty`, `lhopital_at_ninfty`, `lhopital_Ninfty_at_right`, `lhopital_ninfty_at_right`, `lhopital_Ninfty_at_left`, `lhopital_pinfty_at_left`, `lhopital_ninfty_at_left`, `lhopital_Ninfty`, `lhopital_pinfty`, `lhopital_ninfty`, `lhopital_Ninfty_at_pinfty`, `lhopital_ninfty_at_pinfty`, `lhopital_Ninfty_at_ninfty`, `lhopital_pinfty_at_ninfty`, `lhopital_ninfty_at_ninfty`. +- in `realfun.v`: + + lemmas `lhopital_at_pinfty`, `lhopital_at_ninfty`, + `lhopital_Ninfty_at_right`, `lhopital_pinfty_at_right`, `lhopital_ninfty_at_right`, + `lhopital_Ninfty_at_left`, `lhopital_pinfty_at_left`, `lhopital_ninfty_at_left`, + `lhopital_Ninfty`, `lhopital_pinfty`, `lhopital_ninfty`, + `lhopital_Ninfty_at_pinfty`, `lhopital_pinfty_at_pinfty`, `lhopital_ninfty_at_pinfty`, + `lhopital_Ninfty_at_ninfty`, `lhopital_pinfty_at_ninfty`, `lhopital_ninfty_at_ninfty` +- in `lebesgue_Rintegral.v`: + + definition `measure_of_density` + + lemmas `integral_measure_of_density_indic`, + `integral_measure_of_densityMindic`, `sintegral_measure_of_density`, + `integral_measure_of_density` + +- new file `counting_lebesgue.v`: + + lemmas `cstMcounting_esum`, `sintegral_counting_esum`, + `integral_countingT_esum`, `integral_counting_esum` ### Changed diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 080ef6b38e..ee47949c40 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -321,6 +321,7 @@ Qed. End TopologicalLmodule_theory. Section topologicalLmodType_realFieldType. + Context {R : realFieldType} {E : topologicalLmodType R}. Implicit Type x : E. From 7bfe1aba759cd885b56c69b70fd67e349409fdd5 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 7 Jul 2026 16:07:13 +0900 Subject: [PATCH 02/18] haussdorf ctvs --- .../functional_analysis/hahn_banach_theorem.v | 108 +++++++ theories/normedtype_theory/tvs.v | 297 ++++++++++++++++++ 2 files changed, 405 insertions(+) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 378d8e7bc3..2d0e250d45 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -367,6 +367,39 @@ Qed. End hahn_banach_normed. + + +Section line_lmodtype. +Variable (R : numDomainType) (V: lmodType R) (x : V). + +Definition linepred : {pred V} := mem [set y | exists t, y = t *: x ]. +Definition line := {y | linepred y}. + +Lemma line_linepred (y : line) : exists t, val(y) == t *: x. +Proof. +by move: y => [yv] /= /asboolP [t] ->; exists t. +Qed. + + +#[local] Lemma line_submod_closed : submod_closed (linepred). +Proof. +split; first by rewrite inE; exists 0; rewrite scale0r. +move=> t y z; rewrite !inE => -[ty ->] -[tz ->]; exists (t * ty + tz). +by rewrite scalerDl scalerA. +Qed. + +HB.instance Definition _ := + @GRing.isSubmodClosed.Build _ _ linepred line_submod_closed. + + +HB.instance Definition _ := SubChoice.on line. + +HB.instance Definition _ := [SubChoice_isSubLmodule of line by <:]. + +Check (line : lmodType R). +Check (line : subLmodType linepred). +End line_lmodtype. + Section hahn_banach_extension_ctvs. Context {R : realType} {V : convexTvsType R} (F : pred V). (**md Contrary to the normed case, the extension theorem is not true for any @@ -457,3 +490,78 @@ by exists g'. Qed. End hahn_banach_extension_ctvs. + +Check scalerI. +Check scaler_injl. + +(* TBA : to classical *) +Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). +Proof. +move=> a0 ta; apply: contrapT => /eqP t0. +have : t^-1 *: (t *: a) = 0 by rewrite ta scaler0. +by rewrite scalerA mulVf// scale1r; apply/eqP. +Qed. + +Lemma scaleIl (R : numFieldType) (V: lmodType R) (a : V) : a != 0 -> injective (fun t => t *: a). +Proof. +move=> a0 s t => /eqP; rewrite -subr_eq0 -scalerBl => /eqP /(scaler_eq0 a0) /eqP. +by rewrite subr_eq0 => /eqP. +Qed. +(*END TBA *) + +(* 7.2.3 in Jarchow *) +Lemma hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : +(hausdorff_space V) <-> (forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l(x) != 0). +Proof. +split; last first. +(* proof in here is different than in the book - Jarchow mentions "a" continuous seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of the set of seminorm generating the topology - its probably lacks an argument saying that continuous seminorms are always bounded by this set of seminorms, which we haven't formalised here *) + move => H. + pose P := (@seminorm_of R V). + pose P0 := (@seminorm_ofneq0 R V). + suff : hausdorff_space (seminorm_on P0). + have [contVs _ ] := (seminorm_convextvs V). + by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; apply: cs => //. + apply/hausdorff_seminorm_on=> x /H [l]. + have [l0|l0|] := ltrgtP (l x) (0 : R) => //. + have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ (-1 *: l)). + exists p => //; apply: lt_le_trans; last by apply: lp. + by rewrite scaleN1r ltrNr oppr0. + have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ l). + by exists p => //; apply: lt_le_trans; last by apply: lp. +move=> haus x x0. +pose l := fun ( y : line x) => xchoose (line_linepred y). +have llinear: linear_for ( *:%R) l. + rewrite /l /= => t /= u v; apply: scaleIl; first by exact: x0. + rewrite scalerDl -scalerA. + move/eqP: (xchooseP (line_linepred u)) => <-. + move/eqP: (xchooseP (line_linepred v)) => <-. + move/eqP: (xchooseP (line_linepred (t *: u + v))) => <-. + by rewrite (@GRing.valD _ _ (line x)) (*why is it necessary to have the @? *) GRing.valZ. +pose linlP := GRing.isLinear.Build _ _ _ _ l llinear. +pose linl : {linear ((init_subconvextvs (line x))) -> R^o} := HB.pack l linlP. +have lcont : continuous linl. + apply/continuous_closedkernel. + have -> : (linl @^-1` [set 0]) = [set 0]. + apply/seteqP; split => u /=. + move/eqP: (xchooseP (line_linepred u)) => /[swap]; rewrite /l => ->. + by rewrite scale0r -(@GRing.val0 _ _ (line x)) => /val_inj. + move=> u0; move/eqP: (xchooseP (line_linepred u)). + rewrite u0 /= /l; move/eqP; rewrite eq_sym => /eqP. + by move/(scaler_eq0 x0). + apply: accessible_closed_set1; apply: hausdorff_accessible. + by apply: hausdorff_init_convextvs. +pose contlP := isContinuous.Build _ _ _ lcont. +pose lcl : {linear_continuous (init_subconvextvs (line x)) -> R^o} := + HB.pack (l : (init_subconvextvs (line x)) -> R^o) linlP contlP. +have := (hahn_banach_extension_initialsubctvs lcl) => -[g Pg]; exists g. +have xlinepred : (linepred x) x by apply/asboolP; exists 1; rewrite scale1r. +pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. +rewrite Pg. +suff -> : lcl xline = 1 by []. +move/eqP: (xchooseP (line_linepred xline)). +set xline':= (X in X =_ -> _); have -> : xline' = x by []. (*weakness of line, to be understood *) +set x':= (X in X =_ -> _); rewrite -(scale1r x'). +move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. +by apply: H. +Qed. +(* TODO : more hahn banach separation theorems *) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index ee47949c40..642d50c1c3 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -8,6 +8,7 @@ From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import convex set_interval reals topology. From mathcomp Require Import initial_topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. +From mathcomp Require Import contra. (**md**************************************************************************) (* # Topological vector spaces *) @@ -203,6 +204,16 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. + +Lemma accessible_field (K : numFieldType) : accessible_space K^o. +Proof. +move=> x y xy. +exists (ball x (`|x-y|/2)); split; rewrite ?inE /=; first by apply: ball_open. + by apply: ballxx; rewrite mulr_gt0 ?normr_gt0 ?invr_gt0 ?subr_eq0. +rewrite /ball /= ltr_pdivlMr //= gtr_pMr ?normr_gt0 ?subr_eq0 //. +by rewrite ltrn1. +Qed. + Section TopologicalLmodule_theory. Context {R : numFieldType} (E : topologicalLmodType R). @@ -218,6 +229,7 @@ Lemma fun_cvgZr (T : Type) (U : set_system T) {FF : Filter U} k (f : T -> E) a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. + Lemma nbhs0Z (U : set E) (r : R) : r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). Proof. move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. @@ -235,6 +247,50 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. Unshelve. all: by end_near. Qed. +Lemma continuousfor0_continuous (f : {linear F -> G}) : + {for 0, continuous f} -> continuous f. +Proof. +move=> cont0 x. +suff: (f y - f x)@[y --> x] --> (0 : G). + have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G). + by apply: funext => y; rewrite linearB. + move=> fxfy /= A nA /=. + pose B := [set y - f x | y in A]. + have /fxfy : nbhs 0 B. + have -> : B = (+%R^~ (- (- f x))) @^-1` A. + rewrite opprK; apply/seteqP; split. + by move=> y [/= g Ag <-]; rewrite subrK. + move=> g/= Agfx; eexists; first exact: Agfx. + by rewrite addrK. + have:= @continuous_shift _ (0 : G) (f x) A. + by rewrite opprK add0r => /(_ nA); exact. + rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. + by move=> [y Ay]; rewrite linearB => /subIr <-. +have -> : (fun y => f y - f x) = (fun y => f (y - x)). + by apply: funext => y; rewrite linearB. +apply: cvg_comp; last by rewrite -(linear0 f); exact: cont0. +by move => A nA /=; apply: continuous_shift; rewrite subrr. +Qed. + +Lemma hausdorff_convextvs : (hausdorff_space F) <-> closed ([set 0 : F]). +Proof. +split. + move=> /(_ (0:F)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. + move=> a b n0a /(cl b) [? [-> b0]]. + exists 0; split => //; exact: nbhs_singleton. +move => cl. +(* simpler proof using the closed subbasis ?*) +move=> x y H; apply: subr0_eq; have := H. +contra => xy0. +have nxy : nbhs (x-y) (~`[set 0]). + apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. + by apply/eqP. +have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). + by exact: sub_continuous. +move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. +by have := ab0 (z,z) => /=; rewrite subrr; apply. +Qed. + End TopologicalLmodule_theory. Section TopologicalLmodule_numDomain. @@ -501,6 +557,21 @@ HB.instance Definition _ := @Uniform_isConvexTvs.Build R init_subconvextvs locally_convex_sub. HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. +Lemma hausdorff_init_convextvs : hausdorff_space V -> hausdorff_space init_subconvextvs. +Proof. +move=> hV x y; +rewrite /cluster /= /nbhs /= => cl. +apply: val_inj; apply: hV; rewrite nbhsE => A B /= [A' [oA Ax AA']]. +rewrite nbhsE /= => -[B' [oB By BB']]. +have valA: nbhs_of_open (initial_open \val) x (\val @^-1` A'). + by rewrite /nbhs_of_open; exists (\val @^-1` A'); split => //=; exists A'. +have : nbhs_of_open (initial_open \val) y (\val @^-1` B'). + by rewrite /nbhs_of_open; exists (\val @^-1` B'); split => //=; exists B'. +move/(cl (val @^-1` A') (val @^-1` B') valA) => [z /= [Az Bz]]; exists (val z); split. + by apply: AA'. +by apply: BB'. +Qed. + End SubLmodule_isSubConvexTvs. HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E @@ -652,6 +723,7 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. + HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E & GRing.Lmodule R E := { nbhsbasis_at0 : set_system E ; @@ -933,6 +1005,32 @@ HB.end. Section ConvexTvs_realType. +End ConvexTvs_realType. + + +Section ConvexTvs_realType. + +(*better naming ?*) +Lemma scalerx_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : + {for s, continuous (fun t : R^o => t *: x)}. +Proof. +have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + +Lemma scalexr_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : + {for x, continuous (fun y : E => s *: y)}. +Proof. +have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + End ConvexTvs_realType. Section standard_topology. @@ -1258,6 +1356,81 @@ Qed. End openbasis. + +Section closedbasis. +Context (R : realFieldType) (E: convexTvsType R). + +Definition closed_nbhsbasis_ctvs := [set closure b | b in (@nbhsbasis_convextvs R E)]. + +(* TODO : convex is enough and then take balanced closure *) + +Lemma closure_convextvs ( b : set E) : + closure b = \bigcap_(a in (nbhs (0 : E))) (b `+ a). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +apply/seteqP; split => z H. + move=> a' /basis [/=a /[dup] /mem_set /absconv [_ bala]]. + move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. + exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. +move=> d; rewrite nbhsE0=> -[c /basis [/=a /[dup] /mem_set /absconv [_ bala]]]. +move=> /nbhs0 /H [x bx [y ay]] xyz ac zcd. +exists x; split => //; apply: zcd; exists (-y). + by rewrite -scaleN1r; apply/ac/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. +by apply: (addrI y); rewrite addrCA subrr addr0 addrC. +Qed. + +Lemma closure_addsetset (b : set E) : (nbhs 0 b) -> closure b `<=` b `+ b. +Proof. +move=> nb z. rewrite closure_convextvs /bigcap /= => /(_ b nb) [x bx [y by' <-]]. +by exists x => //; exists y. +Qed. + +Lemma has_closed_nbhs_basis : + nbhs_basis 0 closed_nbhsbasis_ctvs + /\ (forall b, closed_nbhsbasis_ctvs b -> (closed b /\ absolutely_convex_set b)). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +split. + split; move=> /= a /=. + by move=> [b /nbhs0 nbhsb <-]; apply: filterS; first by apply: subset_closure. + move=> /nbhs0_add [b] /[dup] /basis [/= c nc cb]. + move=> /closure_addsetset /subset_trans /[apply] cba. + exists (closure c); first by exists c. + apply: subset_trans; last by exact: cba. + by apply: closureS. +move=> ? [c nc <-]; split; first by exact: closed_closure. +have [convc balc] := absconv c (mem_set nc). +split; rewrite /closure. + move => x y t; rewrite !inE /= => Bx By B. + move/nbhsE0 => [a /basis [/= a' na' aa'] aB]. + have [conva _] := absconv a' (mem_set na'). + have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a') !=set0. + apply: (Bx ([set x] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + by move=> z /= [s sa <-]; exists x => //; exists s. + have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a') !=set0. + apply: (By ([set y] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + by move=> // z /= [s sa <-]; exists y => //; exists s. + exists (conv t (cx : convex_lmodType E) cy); split. + by apply/set_mem; apply: convc; rewrite !inE. + apply: aB => /=; rewrite -acy -acx; exists (conv t (ax : convex_lmodType E) ay). + by apply: aa'; apply/set_mem; apply: conva; rewrite !inE. + by rewrite addrACA -!scalerDr. +move=> t t1 ? /= [x Bx] <- B. +have [->|t0] := eqVneq t 0. + by rewrite scale0r => /nbhs_singleton B0; exists 0; split => //; apply: nbhs_singleton; apply: nbhs0. +move/(nbhsZ (invr_neq0 t0)); rewrite scalerA mulrC divff // scale1r. +move/Bx => [z [cz [y by']]] /(congr1 (fun x => t *: x)). +rewrite scalerA divff // scale1r => ytz; exists y; split => //. +rewrite ytz; apply: balc; first by exact: t1. +by exists z. +Qed. + +End closedbasis. + + +Import Norm. + Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) (absA : absolutely_convex_set A) (absorbA : absorbing_set A) : V -> K := fun v => inf [set r | 0 < r /\ v \in (fun x => r *: x) @` A]. @@ -1374,6 +1547,7 @@ End gauge. Definition seminorm_on {R : realFieldType} {E : lmodType R} (P : set (Norm.SemiNorm.type E)) (Hp : P !=set0) : Type := E. + Section convex_topology_seminorm. Context {R : realFieldType} {E : lmodType R} (P : set (Norm.SemiNorm.type E)) (P0 : P !=set0). @@ -1533,6 +1707,39 @@ apply: (@squeeze_cvgr _ (nbhs x)) => /=; first exact: nearp. exact: pshift0. Qed. + +Lemma hausdorff_seminorm_on : +hausdorff_space (seminorm_on H) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). +Proof. +split. + move/hausdorff_convextvs => P0 x; contra => HP. + have : forall p, P p -> p x = 0. + move=> p /HP /negP nlt0. + have:= (@norm_ge0 _ _ p x). + rewrite le0r; case; move/orP => []; first by move/eqP. + by move/nlt0 => //. + move => {HP} HP; apply: P0 => /= c [? [?]] [/= I IB] <- <- xic. + exists 0; split => //; apply: xic => /=; exists x => //; exists (-x); rewrite ?subrr //. + move=> i /= /IB /set_mem /= [p] /HP px0 [e e0] -> /=. + rewrite Theory.normN px0. + by apply: ballxx. +move=> P0; apply/hausdorff_convextvs => x /=; contra => /P0 [p Pp px0]. +exists (p @^-1` ball (p x) (p x)); last first. + by move=> /= ? ->; rewrite norm0 /ball /= subr0 ger0_norm ?norm_ge0 // ltxx. +exists ([set x] `+ p @^-1` ball (0 : R) (p x)); last first. + move=> z /= [? -> [y + <-]]. + rewrite /ball /= sub0r normrN ger0_norm ?norm_ge0 // => pyx. + apply: le_lt_trans; first by apply: Theory.seminorm_normrB. + by rewrite opprD addrA subrr sub0r Theory.normN. +exists (p @^-1` ball (0 : R) (p x)) => //. +exists ([fset (p @^-1` ball (0 : R) (p x))]%fset). + move=> ? ; rewrite inE => /eqP ->; apply/mem_set. + rewrite /seminorm_subbasis /=; exists p => //; exists (p x) => //. +apply/seteqP; split => z /=. + by rewrite /bigcap /= => /(_ (p @^-1` ball (0 : R) (p x))); apply; rewrite inE. +by move=> ballz => ? /=; rewrite inE => /eqP ->. +Qed. + End convex_topology_seminorm. Section generating_seminorm. @@ -1544,6 +1751,7 @@ Definition gauge_fun_basis (b : set E) (h : open_nbhsbasis_convextvs b) := Definition seminorm_of := [set p : Norm.SemiNorm.type E | exists b (h : open_nbhsbasis_convextvs b), p = gauge_fun_basis h]. + #[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E => -[/= b Bb _]. @@ -1739,3 +1947,92 @@ by move/linear_continuous_seminorm => [p [_ cp] lpx]; exists p. Qed. End generating_seminorm. + + +Section kernel. +Context (R : realFieldType) (F : convexTvsType R). +(* Necessary to use has_open_nbhs_basis *) + +(*TBA topology *) +Lemma closed_Ndense (S : set F) : (S != [set: F]) -> closed S -> ~ (dense S). +Proof. +move=> /setTPn [t] nSt. +have S0: (~` S) !=set0 by exists t. +rewrite -openC => /[swap] /(_ _) /[swap] oS /(_ (~` S) S0 oS). +by move=> -[a [+ Sa]]; move=> /(_ Sa). +Qed. + +(* Introduce a notation for kernels ?*) +Lemma continuous_closedkernel (f : {linear F -> R^o}): continuous f <-> closed (f @^-1` [set 0]). +Proof. +split. + move=> /continuous_closedP /(_ [set 0]); apply. + apply: accessible_closed_set1; apply: accessible_field. +have []:= (eqVneq (f @^-1` [set 0]) [set : F]). + move => h _. + suff -> : f = (fun y=> 0) :> (F -> R) by apply: cst_continuous. + apply: funext => x. + have : [set : F] x by []. + by rewrite -h /=. +move=> s0 /closed_Ndense; move=> /(_ s0). +move=> /existsNP [U] /not_implyP [[x Ux]]. +move=> /not_implyP [oU] /forallNP /= Uf. +have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). +have /nbhsE0 [V' /Bbasis [/= V BV VV'] VU]: nbhs x U by rewrite nbhsE; exists U. +have [_ aV]: absolutely_convex_set V by apply: Bconv; rewrite inE. +have nfU: forall z, V z -> f z != f x. + move=> z Vz; apply/eqP => fzx. + have Vnz : V (- z). + rewrite -scaleN1r; apply: aV; last by exists z => //. + by rewrite normrN normr1. + apply: Uf; split; first by apply: VU ; exists (-z); first by apply: VV'. + by rewrite linearB; rewrite fzx subrr. +have [/=M fM]: exists M, forall z, V z -> `|f z | < M. + apply: contrapT; rewrite -forallNE /= => /(_ (`|f x|)) /existsNP [y]. + move=> /not_implyP [Vy] /negP; rewrite -leNgt => fxy. + have fy0 : f y != 0. + apply/eqP => fy0; move: fxy; rewrite fy0 normr0 normr_le0 => /eqP fx0. + by apply: (Uf x); split. + have Vyx : V ((`| f x|/ `| f y|) *: y). + apply: aV; last by exists y. + rewrite ger0_norm ?mulr_ge0 ?invr_ge0 //. + rewrite ler_pdivrMr ?mul1r // normr_gt0; apply/eqP => fy. + have := fxy; rewrite fy normr0 normr_le0 => /eqP fx0. + by apply: (Uf x); split. + have Vnyx : V ( - (`| f x|/ `| f y|) *: y). + apply: aV; last by exists ((`| f x|/ `| f y|) *: y); rewrite // scalerA -mulN1r. + by rewrite normrN normr1. + have [] := ltgtP 0 ((f x)/(f y)). + - move=> fxy0. + apply: (Uf ( x - (`|f x| / `|f y|) *: y)); split. + apply: VU; exists (- (`|f x| / `|f y|) *: y); first by apply: VV'. + by rewrite scaleNr. + rewrite linearD linearN linearZ /=. + have -> : `|f x| / `|f y| = (f x)/(f y) by rewrite -normfV -normrM gtr0_norm. + by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. + - move=> fxy0. + apply: (Uf ( x + (`|f x| / `|f y|) *: y)); split. + by apply: VU; exists ((`|f x| / `|f y|) *: y); first by apply: VV'. + rewrite linearD linearZ /=. + have -> : `|f x| / `|f y| = - (f x)/(f y). + by rewrite -normfV -normrM ltr0_norm ?mulNr. + by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. + - move=> /eqP; rewrite eq_sym mulf_eq0 => /orP [] /eqP. + by move=> fx0; apply: (Uf x); split. + by rewrite -invr0 => /invr_inj fyn0; move/eqP: fy0; apply. +have [M0|M0] := leP M 0 => //. + have := (fM 0); move => /(_ (nbhs_singleton _)); move=> /(_ (B0 V BV)). + by move=> /lt_le_trans /(_ M0); rewrite normr_lt0. +apply: continuousfor0_continuous => /= A; rewrite linear0 => -[r /= r0] rA. +have rM0 : r/ M != 0 by apply: lt0r_neq0; rewrite ?mulr_gt0 ?invr_gt0 //. +apply: (@filterS _ _ _ ( *:%R (r * M^-1) @` V)); last first. + by rewrite -(@scaler0 _ _ (r/M)); apply: nbhsZ; last by apply: B0. +move=> z /= [t] Vt <-; rewrite linearE /=; apply: rA => /=. +rewrite sub0r normrN -[_ *: _]/(_ * _) normrM -ltr_pdivlMl. + by rewrite normr_gt0 //. +rewrite [in X in _ Date: Tue, 20 Oct 2026 22:12:52 +0200 Subject: [PATCH 03/18] fix rebase over seminorm --- .../functional_analysis/hahn_banach_theorem.v | 3 - .../pseudometric_normed_Zmodule.v | 30 ++++- theories/normedtype_theory/tvs.v | 110 ++++-------------- 3 files changed, 50 insertions(+), 93 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 2d0e250d45..1756ad2035 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -491,9 +491,6 @@ Qed. End hahn_banach_extension_ctvs. -Check scalerI. -Check scaler_injl. - (* TBA : to classical *) Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). Proof. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 77cc267fc2..bbb9124ea4 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -6,7 +6,7 @@ From mathcomp Require Import interval interval_inference archimedean. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval ereal reals topology. -From mathcomp Require Import num_normedtype. +From mathcomp Require Import num_normedtype contra. (**md**************************************************************************) (* # Normed topological abelian groups *) @@ -261,6 +261,34 @@ apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]]. by rewrite addrC => /addIr <-. Qed. +Lemma nbhs0_add (A : set M) : nbhs 0 A -> exists2 B, nbhs 0 B & B `+ B `<=` A. +Proof. +move=> na. +have := add_continuous 0 A. +rewrite add0r => /(_ na) /= -[[b1 b2] /= [n1 n2] ba]. +exists (b1 `&` b2); first by apply: filterI. +by move => z /= [x [x1 _]] [y [_ y2]] <-; apply (ba (x,y)); split => /=. +Qed. + +Lemma hausdorff_convextvs : (hausdorff_space M) <-> closed ([set 0 : M]). +Proof. +split. + move=> /(_ (0:M)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. + move=> a b n0a /(cl b) [? [-> b0]]. + exists 0; split => //; exact: nbhs_singleton. +move => cl. +(* simpler proof using the closed subbasis ?*) +move=> x y H; apply: subr0_eq; have := H. +contra => xy0. +have nxy : nbhs (x-y) (~`[set 0]). + apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. + by apply/eqP. +have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). + by exact: sub_continuous. +move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. +by have := ab0 (z,z) => /=; rewrite subrr; apply. +Qed. + End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 642d50c1c3..52b34f07cf 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -214,6 +214,7 @@ rewrite /ball /= ltr_pdivlMr //= gtr_pMr ?normr_gt0 ?subr_eq0 //. by rewrite ltrn1. Qed. + Section TopologicalLmodule_theory. Context {R : numFieldType} (E : topologicalLmodType R). @@ -229,7 +230,6 @@ Lemma fun_cvgZr (T : Type) (U : set_system T) {FF : Filter U} k (f : T -> E) a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. - Lemma nbhs0Z (U : set E) (r : R) : r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). Proof. move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. @@ -247,50 +247,6 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. Unshelve. all: by end_near. Qed. -Lemma continuousfor0_continuous (f : {linear F -> G}) : - {for 0, continuous f} -> continuous f. -Proof. -move=> cont0 x. -suff: (f y - f x)@[y --> x] --> (0 : G). - have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G). - by apply: funext => y; rewrite linearB. - move=> fxfy /= A nA /=. - pose B := [set y - f x | y in A]. - have /fxfy : nbhs 0 B. - have -> : B = (+%R^~ (- (- f x))) @^-1` A. - rewrite opprK; apply/seteqP; split. - by move=> y [/= g Ag <-]; rewrite subrK. - move=> g/= Agfx; eexists; first exact: Agfx. - by rewrite addrK. - have:= @continuous_shift _ (0 : G) (f x) A. - by rewrite opprK add0r => /(_ nA); exact. - rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. - by move=> [y Ay]; rewrite linearB => /subIr <-. -have -> : (fun y => f y - f x) = (fun y => f (y - x)). - by apply: funext => y; rewrite linearB. -apply: cvg_comp; last by rewrite -(linear0 f); exact: cont0. -by move => A nA /=; apply: continuous_shift; rewrite subrr. -Qed. - -Lemma hausdorff_convextvs : (hausdorff_space F) <-> closed ([set 0 : F]). -Proof. -split. - move=> /(_ (0:F)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. - move=> a b n0a /(cl b) [? [-> b0]]. - exists 0; split => //; exact: nbhs_singleton. -move => cl. -(* simpler proof using the closed subbasis ?*) -move=> x y H; apply: subr0_eq; have := H. -contra => xy0. -have nxy : nbhs (x-y) (~`[set 0]). - apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. - by apply/eqP. -have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). - by exact: sub_continuous. -move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. -by have := ab0 (z,z) => /=; rewrite subrr; apply. -Qed. - End TopologicalLmodule_theory. Section TopologicalLmodule_numDomain. @@ -1002,37 +958,6 @@ HB.instance Definition _ := @NbhsBasisAt0_isConvexTvs.Build R E HB.end. -Section ConvexTvs_realType. - - -End ConvexTvs_realType. - - -Section ConvexTvs_realType. - -(*better naming ?*) -Lemma scalerx_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : - {for s, continuous (fun t : R^o => t *: x)}. -Proof. -have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). - exact: funext. -apply: continuous_comp. -apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. -exact: (scale_continuous (s, x)). -Qed. - -Lemma scalexr_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : - {for x, continuous (fun y : E => s *: y)}. -Proof. -have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). - exact: funext. -apply: continuous_comp. -apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. -exact: (scale_continuous (s, x)). -Qed. - -End ConvexTvs_realType. - Section standard_topology. Context {R : numFieldType}. @@ -1290,7 +1215,7 @@ End lcfunproperties. Local Open Scope convex_scope. Section openbasis. -Context (R : realType) (E : convexTvsType R). +Context (R : realFieldType) (E : convexTvsType R). Definition nbhsbasis_convextvs := sval (cid2 (@locally_convex _ E)). @@ -1373,10 +1298,11 @@ apply/seteqP; split => z H. move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. -move=> d; rewrite nbhsE0=> -[c /basis [/=a /[dup] /mem_set /absconv [_ bala]]]. -move=> /nbhs0 /H [x bx [y ay]] xyz ac zcd. +move=> d; rewrite nbhsE0. +move => [dz] [/=a /basis [ /= a'/[dup] /mem_set /= /absconv [_ bala]]]. +move=> /nbhs0 /H [x bx [y ay]] xyz aa' zcd. exists x; split => //; apply: zcd; exists (-y). - by rewrite -scaleN1r; apply/ac/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. by apply: (addrI y); rewrite addrCA subrr addr0 addrC. Qed. @@ -1403,18 +1329,24 @@ move=> ? [c nc <-]; split; first by exact: closed_closure. have [convc balc] := absconv c (mem_set nc). split; rewrite /closure. move => x y t; rewrite !inE /= => Bx By B. - move/nbhsE0 => [a /basis [/= a' na' aa'] aB]. - have [conva _] := absconv a' (mem_set na'). - have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a') !=set0. - apply: (Bx ([set x] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + move/nbhsE0 => [Bxy [b /basis [/= a /[dup ]/nbhs0 na0 na ab] aB]]. + have [conva _] := absconv a (mem_set na). + have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a) !=set0. + apply: (Bx ([set x] `+ a)); rewrite nbhsE0; split. + exists x => //=; exists 0; last by rewrite addr0. + by apply: nbhs_singleton. + exists a; first by apply: nbhs0. by move=> z /= [s sa <-]; exists x => //; exists s. - have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a') !=set0. - apply: (By ([set y] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a ) !=set0. + apply: (By ([set y] `+ a )); rewrite nbhsE0; split. + exists y => //=; exists 0; last by rewrite addr0. + by apply: nbhs_singleton => //=. + exists a ; first by apply: nbhs0. by move=> // z /= [s sa <-]; exists y => //; exists s. exists (conv t (cx : convex_lmodType E) cy); split. by apply/set_mem; apply: convc; rewrite !inE. apply: aB => /=; rewrite -acy -acx; exists (conv t (ax : convex_lmodType E) ay). - by apply: aa'; apply/set_mem; apply: conva; rewrite !inE. + by apply: ab; apply/set_mem; apply: conva; rewrite !inE. by rewrite addrACA -!scalerDr. move=> t t1 ? /= [x Bx] <- B. have [->|t0] := eqVneq t 0. @@ -1752,7 +1684,7 @@ Definition seminorm_of := [set p : Norm.SemiNorm.type E | exists b (h : open_nbhsbasis_convextvs b), p = gauge_fun_basis h]. -#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. +Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E => -[/= b Bb _]. by exists (gauge_fun_basis Bb), b, Bb. @@ -1978,7 +1910,7 @@ move=> s0 /closed_Ndense; move=> /(_ s0). move=> /existsNP [U] /not_implyP [[x Ux]]. move=> /not_implyP [oU] /forallNP /= Uf. have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). -have /nbhsE0 [V' /Bbasis [/= V BV VV'] VU]: nbhs x U by rewrite nbhsE; exists U. +have /nbhsE0 [_ [V' /Bbasis [/= V BV VV'] VU]]: nbhs x U by rewrite nbhsE; exists U. have [_ aV]: absolutely_convex_set V by apply: Bconv; rewrite inE. have nfU: forall z, V z -> f z != f x. move=> z Vz; apply/eqP => fzx. From d046b1dea701284ff716d69ffd3d61548efb9fac Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 23 Oct 2026 22:42:21 +0200 Subject: [PATCH 04/18] rebase on seminorm_tvs --- theories/functional_analysis/hahn_banach_theorem.v | 4 ++-- theories/normedtype_theory/tvs.v | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 1756ad2035..55bf1632e2 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -1,4 +1,4 @@ -From HB Require Import structures. +From HB Require Import structures. From mathcomp Require Import boot order algebra interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -516,7 +516,7 @@ split; last first. pose P := (@seminorm_of R V). pose P0 := (@seminorm_ofneq0 R V). suff : hausdorff_space (seminorm_on P0). - have [contVs _ ] := (seminorm_convextvs V). + have [contVs _ ] := (@seminorm_convextvs _ V). by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; apply: cs => //. apply/hausdorff_seminorm_on=> x /H [l]. have [l0|l0|] := ltrgtP (l x) (0 : R) => //. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 52b34f07cf..6863fbbd24 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1641,21 +1641,21 @@ Qed. Lemma hausdorff_seminorm_on : -hausdorff_space (seminorm_on H) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). +hausdorff_space (seminorm_on P0) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). Proof. split. - move/hausdorff_convextvs => P0 x; contra => HP. + move/hausdorff_convextvs => H0 x; contra => HP. have : forall p, P p -> p x = 0. move=> p /HP /negP nlt0. have:= (@norm_ge0 _ _ p x). rewrite le0r; case; move/orP => []; first by move/eqP. by move/nlt0 => //. - move => {HP} HP; apply: P0 => /= c [? [?]] [/= I IB] <- <- xic. + move => {HP} HP; apply: H0 => /= c [? [?]] [/= I IB] <- <- xic. exists 0; split => //; apply: xic => /=; exists x => //; exists (-x); rewrite ?subrr //. move=> i /= /IB /set_mem /= [p] /HP px0 [e e0] -> /=. rewrite Theory.normN px0. by apply: ballxx. -move=> P0; apply/hausdorff_convextvs => x /=; contra => /P0 [p Pp px0]. +move=> H0; apply/hausdorff_convextvs => x /=; contra => /H0 [p Pp px0]. exists (p @^-1` ball (p x) (p x)); last first. by move=> /= ? ->; rewrite norm0 /ball /= subr0 ger0_norm ?norm_ge0 // ltxx. exists ([set x] `+ p @^-1` ball (0 : R) (p x)); last first. From ab02c7bb385ecd0f2dc1e5bde0bf74568daaf82c Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 2 Nov 2026 10:09:48 +0100 Subject: [PATCH 05/18] clean --- .../functional_analysis/hahn_banach_theorem.v | 21 ++++++---- theories/normedtype_theory/tvs.v | 41 ++++++------------- theories/topology_theory/topology_structure.v | 9 ++++ 3 files changed, 34 insertions(+), 37 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 55bf1632e2..7e04bdb6b9 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -370,6 +370,9 @@ End hahn_banach_normed. Section line_lmodtype. +(**md this section construct the subLmodType structure on a line generated by an +element of a lmodType. It is necessary to prove hahn_banach_separation_hausdorff +below *) Variable (R : numDomainType) (V: lmodType R) (x : V). Definition linepred : {pred V} := mem [set y | exists t, y = t *: x ]. @@ -380,7 +383,6 @@ Proof. by move: y => [yv] /= /asboolP [t] ->; exists t. Qed. - #[local] Lemma line_submod_closed : submod_closed (linepred). Proof. split; first by rewrite inE; exists 0; rewrite scale0r. @@ -391,13 +393,10 @@ Qed. HB.instance Definition _ := @GRing.isSubmodClosed.Build _ _ linepred line_submod_closed. - HB.instance Definition _ := SubChoice.on line. HB.instance Definition _ := [SubChoice_isSubLmodule of line by <:]. -Check (line : lmodType R). -Check (line : subLmodType linepred). End line_lmodtype. Section hahn_banach_extension_ctvs. @@ -511,7 +510,11 @@ Lemma hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : (hausdorff_space V) <-> (forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l(x) != 0). Proof. split; last first. -(* proof in here is different than in the book - Jarchow mentions "a" continuous seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of the set of seminorm generating the topology - its probably lacks an argument saying that continuous seminorms are always bounded by this set of seminorms, which we haven't formalised here *) +(* proof in here is different than in the book - Jarchow mentions "a" continuous +seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of +the set of seminorm generating the topology - its probably lacks an argument +saying that continuous seminorms are always bounded by this set of seminorms, +which we haven't formalised here *) move => H. pose P := (@seminorm_of R V). pose P0 := (@seminorm_ofneq0 R V). @@ -520,7 +523,7 @@ split; last first. by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; apply: cs => //. apply/hausdorff_seminorm_on=> x /H [l]. have [l0|l0|] := ltrgtP (l x) (0 : R) => //. - have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ (-1 *: l)). + have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ (-1 *: l)). exists p => //; apply: lt_le_trans; last by apply: lp. by rewrite scaleN1r ltrNr oppr0. have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ l). @@ -533,7 +536,7 @@ have llinear: linear_for ( *:%R) l. move/eqP: (xchooseP (line_linepred u)) => <-. move/eqP: (xchooseP (line_linepred v)) => <-. move/eqP: (xchooseP (line_linepred (t *: u + v))) => <-. - by rewrite (@GRing.valD _ _ (line x)) (*why is it necessary to have the @? *) GRing.valZ. + by rewrite (@GRing.valD _ _ (line x)) GRing.valZ. pose linlP := GRing.isLinear.Build _ _ _ _ l llinear. pose linl : {linear ((init_subconvextvs (line x))) -> R^o} := HB.pack l linlP. have lcont : continuous linl. @@ -556,9 +559,11 @@ pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. rewrite Pg. suff -> : lcl xline = 1 by []. move/eqP: (xchooseP (line_linepred xline)). -set xline':= (X in X =_ -> _); have -> : xline' = x by []. (*weakness of line, to be understood *) +set xline':= (X in X =_ -> _); have -> : xline' = x by []. +(*TODO weakness of line, to be understood *) set x':= (X in X =_ -> _); rewrite -(scale1r x'). move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. by apply: H. Qed. + (* TODO : more hahn banach separation theorems *) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 6863fbbd24..84e5ba4b17 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -515,17 +515,16 @@ HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. Lemma hausdorff_init_convextvs : hausdorff_space V -> hausdorff_space init_subconvextvs. Proof. -move=> hV x y; -rewrite /cluster /= /nbhs /= => cl. +move=> hV x y; rewrite /cluster /= /nbhs /= => cl. apply: val_inj; apply: hV; rewrite nbhsE => A B /= [A' [oA Ax AA']]. rewrite nbhsE /= => -[B' [oB By BB']]. have valA: nbhs_of_open (initial_open \val) x (\val @^-1` A'). by rewrite /nbhs_of_open; exists (\val @^-1` A'); split => //=; exists A'. have : nbhs_of_open (initial_open \val) y (\val @^-1` B'). by rewrite /nbhs_of_open; exists (\val @^-1` B'); split => //=; exists B'. -move/(cl (val @^-1` A') (val @^-1` B') valA) => [z /= [Az Bz]]; exists (val z); split. - by apply: AA'. -by apply: BB'. +move/(cl (val @^-1` A') (val @^-1` B') valA) => [z /= [Az Bz]]; exists (val z). +split; first exact: AA'. +exact: BB'. Qed. End SubLmodule_isSubConvexTvs. @@ -1883,31 +1882,19 @@ End generating_seminorm. Section kernel. Context (R : realFieldType) (F : convexTvsType R). -(* Necessary to use has_open_nbhs_basis *) - -(*TBA topology *) -Lemma closed_Ndense (S : set F) : (S != [set: F]) -> closed S -> ~ (dense S). -Proof. -move=> /setTPn [t] nSt. -have S0: (~` S) !=set0 by exists t. -rewrite -openC => /[swap] /(_ _) /[swap] oS /(_ (~` S) S0 oS). -by move=> -[a [+ Sa]]; move=> /(_ Sa). -Qed. (* Introduce a notation for kernels ?*) Lemma continuous_closedkernel (f : {linear F -> R^o}): continuous f <-> closed (f @^-1` [set 0]). Proof. split. move=> /continuous_closedP /(_ [set 0]); apply. - apply: accessible_closed_set1; apply: accessible_field. + by apply: accessible_closed_set1; apply: accessible_field. have []:= (eqVneq (f @^-1` [set 0]) [set : F]). move => h _. suff -> : f = (fun y=> 0) :> (F -> R) by apply: cst_continuous. apply: funext => x. - have : [set : F] x by []. - by rewrite -h /=. -move=> s0 /closed_Ndense; move=> /(_ s0). -move=> /existsNP [U] /not_implyP [[x Ux]]. + by have : [set : F] x by []; rewrite -h. +move=> s0 /closed_Ndense; move=> /(_ s0) /existsNP [U] /not_implyP [[x Ux]]. move=> /not_implyP [oU] /forallNP /= Uf. have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). have /nbhsE0 [_ [V' /Bbasis [/= V BV VV'] VU]]: nbhs x U by rewrite nbhsE; exists U. @@ -1934,22 +1921,20 @@ have [/=M fM]: exists M, forall z, V z -> `|f z | < M. have Vnyx : V ( - (`| f x|/ `| f y|) *: y). apply: aV; last by exists ((`| f x|/ `| f y|) *: y); rewrite // scalerA -mulN1r. by rewrite normrN normr1. - have [] := ltgtP 0 ((f x)/(f y)). - - move=> fxy0. - apply: (Uf ( x - (`|f x| / `|f y|) *: y)); split. + have [fxy0|fxy0|/eqP] := ltgtP 0 ((f x)/(f y)). + - apply: (Uf ( x - (`|f x| / `|f y|) *: y)); split. apply: VU; exists (- (`|f x| / `|f y|) *: y); first by apply: VV'. by rewrite scaleNr. rewrite linearD linearN linearZ /=. have -> : `|f x| / `|f y| = (f x)/(f y) by rewrite -normfV -normrM gtr0_norm. by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. - - move=> fxy0. - apply: (Uf ( x + (`|f x| / `|f y|) *: y)); split. + - apply: (Uf ( x + (`|f x| / `|f y|) *: y)); split. by apply: VU; exists ((`|f x| / `|f y|) *: y); first by apply: VV'. rewrite linearD linearZ /=. have -> : `|f x| / `|f y| = - (f x)/(f y). by rewrite -normfV -normrM ltr0_norm ?mulNr. by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. - - move=> /eqP; rewrite eq_sym mulf_eq0 => /orP [] /eqP. + - rewrite eq_sym mulf_eq0 => /orP [] /eqP. by move=> fx0; apply: (Uf x); split. by rewrite -invr0 => /invr_inj fyn0; move/eqP: fy0; apply. have [M0|M0] := leP M 0 => //. @@ -1960,11 +1945,9 @@ have rM0 : r/ M != 0 by apply: lt0r_neq0; rewrite ?mulr_gt0 ?invr_gt0 //. apply: (@filterS _ _ _ ( *:%R (r * M^-1) @` V)); last first. by rewrite -(@scaler0 _ _ (r/M)); apply: nbhsZ; last by apply: B0. move=> z /= [t] Vt <-; rewrite linearE /=; apply: rA => /=. -rewrite sub0r normrN -[_ *: _]/(_ * _) normrM -ltr_pdivlMl. - by rewrite normr_gt0 //. +rewrite sub0r normrN -[_ *: _]/(_ * _) normrM -ltr_pdivlMl ?normr_gt0 //. rewrite [in X in _ -[]. Qed. +Lemma closed_Ndense (T : topologicalType) (A : set T) : + (A != [set: T]) -> closed A -> ~ (dense A). +Proof. +move=> /setTPn [t] nAt. +have A0: (~` A) !=set0 by exists t. +rewrite -openC => /[swap] /(_ _) /[swap] oA /(_ (~` A) A0 oA). +by move=> -[a [+ Aa]]; move=> /(_ Aa). +Qed. + Section basis. Context {T : topologicalType}. From 15cb42194fb8f062b7017a6179adb541ad158256 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 5 Nov 2026 15:38:40 +0100 Subject: [PATCH 06/18] changelog and clean --- CHANGELOG_UNRELEASED.md | 237 ++---------------- .../functional_analysis/hahn_banach_theorem.v | 8 +- theories/normedtype_theory/tvs.v | 66 ++--- 3 files changed, 63 insertions(+), 248 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f2201b196e..051d381010 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,6 +3,29 @@ ## [Unreleased] ### Added +- in `topology_structure.v` + + lemma `closed_Ndense` + +- in `pseudometric_normed_Zmodule.v` + + lemma `nbhs0_add` + + lemma `hausdorff_convextvs` + +- in `tvs.v` + + lemma `closure_convextvs`, `closure_addset` + + lemma ` accessible field` + + lemma `hausdorff_init_convextvs` + + definition `closed_nbhsbasis_convextvs` + + lemma `has_closed_nbhs_basis` + + lemma `hausdorff_seminorm_on` + + lemma `seminorm_of_neq0` + + lemma `continuous_closedkernel` + +- in `hahn_banach_theorem.v` + + definition `linepred` and `line` + + lemma `line_linepred` + + subLmodule structure on `line` + + lemma `scaler_eq0` and `sclaeIl` (TO BE MOVED) + + lemma hahn_banach_extension_hausdorff - in `exp.v`: + lemmas `cvgy_expR`, `cvgNy_expR`, `lny`, `ge0_lt1_powR_cvg0`, @@ -11,218 +34,6 @@ + instance `is_derive1_powRl` - in `ereal_normedtype.v`: + lemma `ge0_cvgMly` -- in `unstable.v`: - + lemma `itv_boundlr_lt`, - + module `EndlessDense` - * definitions `is_endless`, `is_dense` - * lemmas `itv_bound_half_dense` - * defintions `dual_itv_bound`, `dual_itv` - * lemmas `dual_itvE`, `dual_itv_sub_memP`, `dual_is_dense`, `dual_is_endless`, - ` dual_itv_boundK`, `dual_itv_bound_lt`, `dual_itv_bound_le` - * lemmas `subitvP`, `numDomain_is_endless`, `numField_is_dense` - + lemma `real_subitvP` - -- in `classical_sets.v`: - + lemma `powerset0`, `powerset1`, `powerset2`, `powersetS`, - `setorder_itv_setUl_image`, `setorder_itv_setUr_image`, - `setorder_itv_setDl_image` - -- in set_interval.v - + lemmas `itv_open_endsPn`, `itv_closed_endsPn`, `itv_open_ends_boundlr` - -- in topology_structure.v - + lemmas `closureEbigcap_itvcy`,`interiorEbigcup_itvNyc`, - `closureEbigcap_itvcc`,`interiorEbigcup_itvcc` - -- in num_topology.v - + module `EndlessDenseTopology` (internal) - + lemmas `open_itv_open_ends`, `closed_itv_closed_ends`, - `itv_closureE`, `itv_interiorE` - -- in `sequences.v`: - + lemma `sdrop_shift` - + lemma `ge_einfs` - + lemma `einfs_shift` - + lemma `limn_einf_shift_new` - + lemma `limn_einf_shiftS` - + lemma `limn_einf_cst` -- in `uniform_structure.v`: - + lemma `unif_continuous_continuous` -- in `uniform_structure.v`: - + lemma `unif_continuous_comp` - -- in `initial_topology.v`: - + lemma `initial_unif_continuous` - + lemma `initial_unif_continuous_comp` - + lemma `initial_unif_continuous_comp_fst` - + lemma `initial_unif_continuous_comp_snd` - + lemma `initial_nbhs_preimage` - -- in `product_topology.v`: - + lemma `entourage_prod_exS` - + definition `interchange_prod` - + lemma `entourage_interchange_prod` - + lemma `pair_unif_continuous` - + lemma `fst_unif_continuous` - + lemma `snd_unif_continuous` - -- in `metric_space.v`: - + definition `prod_mdist` - -- in `pseudometric_normed_Zmodule.v`: - + lemma `PseudoMetricNormedZmodule_add_unif_continuous` - + lemma `PseudoMetricNormedZmodule_opp_unif_continuous` - + lemma `standard_scale_continuous` - + notation `topologicalNmodType` - -- in `sequences.v`, - + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` - -- in `num_normedtype.v`, - + lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, - `lt0_cvgMrNy`, `lt0_cvgMly`, `lt0_cvgMry` - -- in `pseudometric_normed_Zmodule.v`, - + lemmas `fmap_at_left0P`, `fmap_at_right0E` - -- in `unstable.v`: - + definitions `clamp`, `clamp_gele` - + lemmas `clamp_gemin`, `clamp_lemax`, `minmax_clamp`, - `clamp_id`, `clamp_min`, `clamp_max` - + lemma `seminorm_normrB` - -- in `topology_structure.v`: - + lemma `id_continuous` - + definition `nbhs_basis` - + definition `openU_from` - -- in `normed_module.v`: - + lemma `ball_convex_set` (was a `Let`) - -- in `classical_sets.v`: - + notation ``... `+ ...`` - + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA` - -- in `convex.v`: - + lemmas `lt_conv`, `le_conv` - + lemma `convD` - -- in `pseudmetric_normed_Zmodule.v`: - + lemma `continuous_shift` - + lemma `nbhs_add1set` - -- in `tvs.v`: - + definition `balanced_set` - + definition `absolutely_convex_set` - + lemma `absolutely_convex0` - + definition `absorbing_set` - + lemma `absolutely_convex_setX` - + definition `init_subconvextvs` - + factory `NbhsBasisAt0_isConvexTvs` - + definition `filter_from_basis0` - + factory `NbhsSubbasisAt0_isConvexTvs` - + definition `finI_fromsubbasis0` - + lemma `openD` - + lemma `openB` - + lemma `nbhsE0` - + lemma `openZ` - + lemma `continuousZl` - + lemma `continuousZr` - + lemma `scalerx_continuous` - + lemma `scalexr_continuous` - + definition `nbhsbasis_convextvs` - + definition `open_nbhsbasis_convextvs` - + definition `open_absconvex_opennbhsbasis` - + definition `basis_opennbhsbasis` - + lemma `basis_neqset0` - + lemma `absorbing_opennbhsbasis` - + definition `gauge_fun` - + definition `seminorm_on` - + definition `seminorm_subbasis` - + lemmas `nonempty_subbasis`, `mem0_seminorm_subbasis`, `split_seminorm_subbasis`, - `expand_seminorm_subbasis` - + lemmas `convex_seminorm_subbasis`, `balanced_seminorm_subbasis`, - `absolutely_convex_seminorm_subbasis`, `absorbing_seminorm`, `continuous_at0_seminorm`, - `continuous_seminorm` - + definitions `gauge_fun_basis`, `seminorm_of` - + theorem `seminorm_convextvs` - + lemma `continuous_seminorm_of` - + lemma `linear_continuous_seminorm` - + lemma `linear_seminorm_continuous` - + proposition `lcfun_seminorm` - -- in `hahn_banach_theorem.v` - + theorem `hahn_banach_extension_subctvs` - + theorem `hahn_banach_extension_initialsubctvs` - -- in `sequences.v`, - + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` - -- new file `edist.v` -- in `classical_sets.v` - + lemma `bigcup_idset1` - -- in `esum.v`: - + lemma `nonempty_esumy` - + lemma `infinite_esum_cst` - -- in `random_variable.v`: - + lemma `not_range_pmf0` - + lemma `dRV_esum_pmf_distribution` - -- in `measure_theory/measure_function.v`: - + lemma `semi_cvg_measure_bigcap` -- in `num_normedtype.v`: - + `continuous_within_itvbbP`, - `continuous_within_itvocP`, `continuous_within_itvcoP`, - `continuous_within_itvbyP`, `continuous_within_itvNybP` -- in `num_topology.v`: - + lemma `not_nearP` - + lemma `not_nearPball` -- in `pseudometric_structure.v`: - + lemma `cvg_withinP` - -- in `ftc.v`: - + lemma `integration_by_partsy_ge0_ge0` - + lemma `integration_by_partsy_le0_ge0` - + lemma `integration_by_partsy_le0_le0` - + lemma `integration_by_partsy_ge0_le0` - -- in `realfun.v`: - + lemma `derivable_oy_RcontinuousN` - -- in `topology_structure.v`: - + definitions `separable_set`, `separable` - + lemmas `basisP`, `separableTE`, `second_countable_separable`, - `bigcupT_separable`, `bigcup_separable` -- 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`, `at_right_shift`, `near_right_in_itv`, and `near_left_in_itv`. -- in file `nat_topology.v`: - + lemma `near_infty_after` - -- in file `realfun.v`: - + new lemmas `lhopital_at_pinfty`, `lhopital_at_ninfty`, `lhopital_Ninfty_at_right`, `lhopital_ninfty_at_right`, `lhopital_Ninfty_at_left`, `lhopital_pinfty_at_left`, `lhopital_ninfty_at_left`, `lhopital_Ninfty`, `lhopital_pinfty`, `lhopital_ninfty`, `lhopital_Ninfty_at_pinfty`, `lhopital_ninfty_at_pinfty`, `lhopital_Ninfty_at_ninfty`, `lhopital_pinfty_at_ninfty`, `lhopital_ninfty_at_ninfty`. -- in `realfun.v`: - + lemmas `lhopital_at_pinfty`, `lhopital_at_ninfty`, - `lhopital_Ninfty_at_right`, `lhopital_pinfty_at_right`, `lhopital_ninfty_at_right`, - `lhopital_Ninfty_at_left`, `lhopital_pinfty_at_left`, `lhopital_ninfty_at_left`, - `lhopital_Ninfty`, `lhopital_pinfty`, `lhopital_ninfty`, - `lhopital_Ninfty_at_pinfty`, `lhopital_pinfty_at_pinfty`, `lhopital_ninfty_at_pinfty`, - `lhopital_Ninfty_at_ninfty`, `lhopital_pinfty_at_ninfty`, `lhopital_ninfty_at_ninfty` -- in `lebesgue_Rintegral.v`: - + definition `measure_of_density` - + lemmas `integral_measure_of_density_indic`, - `integral_measure_of_densityMindic`, `sintegral_measure_of_density`, - `integral_measure_of_density` - -- new file `counting_lebesgue.v`: - + lemmas `cstMcounting_esum`, `sintegral_counting_esum`, - `integral_countingT_esum`, `integral_counting_esum` ### Changed @@ -255,4 +66,4 @@ ### Infrastructure -### Misc +### Misc \ No newline at end of file diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 7e04bdb6b9..6a7d1ac8f1 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -1,4 +1,4 @@ -From HB Require Import structures. +From HB Require Import structures. From mathcomp Require Import boot order algebra interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -27,6 +27,10 @@ From mathcomp Require Import reals convex topology normedtype. (* | hahn_banach_extension_normed | subNormedmodType | normedModType |*) (* | hahn_banach_extension_subcvts | subconvextvsType | convexTvsType |*) (* | hahn_banach_extension_initialsubctvs | subLmodType | convexTvsType |*) +(* *) +(* Theorem `hahn_banach_extension_hausdorff` states, given a non-null point *) +(* in a convexTvsType, the existence of a linear continuous form non-null at *) +(* this point. *) (******************************************************************************) Set Implicit Arguments. @@ -490,7 +494,7 @@ Qed. End hahn_banach_extension_ctvs. -(* TBA : to classical *) +(* TBA : to classical ? Where shoudl this go *) Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). Proof. move=> a0 ta; apply: contrapT => /eqP t0. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 84e5ba4b17..114a4570db 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -214,7 +214,6 @@ rewrite /ball /= ltr_pdivlMr //= gtr_pMr ?normr_gt0 ?subr_eq0 //. by rewrite ltrn1. Qed. - Section TopologicalLmodule_theory. Context {R : numFieldType} (E : topologicalLmodType R). @@ -333,7 +332,6 @@ Qed. End TopologicalLmodule_theory. Section topologicalLmodType_realFieldType. - Context {R : realFieldType} {E : topologicalLmodType R}. Implicit Type x : E. @@ -403,6 +401,34 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U }. +Section ConvexTvs_theory. +Context (R : numFieldType) (E : convexTvsType R). + +Lemma closure_convextvs (b : set E) : + closure b = \bigcap_(a in (nbhs (0 : E))) (b `+ a). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +apply/seteqP; split => z H. + move=> a' /basis [/=a /[dup] /mem_set /absconv [_ bala]]. + move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. + exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. +move=> d; rewrite nbhsE0. +move => [dz] [/=a /basis [ /= a'/[dup] /mem_set /= /absconv [_ bala]]]. +move=> /nbhs0 /H [x bx [y ay]] xyz aa' zcd. +exists x; split => //; apply: zcd; exists (-y). + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. +by apply: (addrI y); rewrite addrCA subrr addr0 addrC. +Qed. + +Lemma closure_addset (b : set E) : (nbhs 0 b) -> closure b `<=` b `+ b. +Proof. +move=> nb z; rewrite closure_convextvs /bigcap /= => /(_ b nb) [x bx [y by' <-]]. +by exists x => //; exists y. +Qed. + +End ConvexTvs_theory. + Section SubLmodule_isSubConvexTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). @@ -678,7 +704,6 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. - HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E & GRing.Lmodule R E := { nbhsbasis_at0 : set_system E ; @@ -1282,34 +1307,12 @@ End openbasis. Section closedbasis. +(* This section shows that every convexTvsType admits a basis of closed +absolutely convex sets *) Context (R : realFieldType) (E: convexTvsType R). -Definition closed_nbhsbasis_ctvs := [set closure b | b in (@nbhsbasis_convextvs R E)]. - -(* TODO : convex is enough and then take balanced closure *) - -Lemma closure_convextvs ( b : set E) : - closure b = \bigcap_(a in (nbhs (0 : E))) (b `+ a). -Proof. -have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). -apply/seteqP; split => z H. - move=> a' /basis [/=a /[dup] /mem_set /absconv [_ bala]]. - move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. - exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. - by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. -move=> d; rewrite nbhsE0. -move => [dz] [/=a /basis [ /= a'/[dup] /mem_set /= /absconv [_ bala]]]. -move=> /nbhs0 /H [x bx [y ay]] xyz aa' zcd. -exists x; split => //; apply: zcd; exists (-y). - by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. -by apply: (addrI y); rewrite addrCA subrr addr0 addrC. -Qed. - -Lemma closure_addsetset (b : set E) : (nbhs 0 b) -> closure b `<=` b `+ b. -Proof. -move=> nb z. rewrite closure_convextvs /bigcap /= => /(_ b nb) [x bx [y by' <-]]. -by exists x => //; exists y. -Qed. +Definition closed_nbhsbasis_ctvs := + [set closure b | b in (@nbhsbasis_convextvs R E)]. Lemma has_closed_nbhs_basis : nbhs_basis 0 closed_nbhsbasis_ctvs @@ -1320,7 +1323,7 @@ split. split; move=> /= a /=. by move=> [b /nbhs0 nbhsb <-]; apply: filterS; first by apply: subset_closure. move=> /nbhs0_add [b] /[dup] /basis [/= c nc cb]. - move=> /closure_addsetset /subset_trans /[apply] cba. + move=> /closure_addset /subset_trans /[apply] cba. exists (closure c); first by exists c. apply: subset_trans; last by exact: cba. by apply: closureS. @@ -1359,9 +1362,6 @@ Qed. End closedbasis. - -Import Norm. - Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) (absA : absolutely_convex_set A) (absorbA : absorbing_set A) : V -> K := fun v => inf [set r | 0 < r /\ v \in (fun x => r *: x) @` A]. From e3158d8d112f8bd0001993a57ffd10137ae4b294 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 5 Nov 2026 15:43:10 +0100 Subject: [PATCH 07/18] clean --- theories/normedtype_theory/tvs.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 114a4570db..82034c6784 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1478,7 +1478,6 @@ End gauge. Definition seminorm_on {R : realFieldType} {E : lmodType R} (P : set (Norm.SemiNorm.type E)) (Hp : P !=set0) : Type := E. - Section convex_topology_seminorm. Context {R : realFieldType} {E : lmodType R} (P : set (Norm.SemiNorm.type E)) (P0 : P !=set0). @@ -1638,7 +1637,6 @@ apply: (@squeeze_cvgr _ (nbhs x)) => /=; first exact: nearp. exact: pshift0. Qed. - Lemma hausdorff_seminorm_on : hausdorff_space (seminorm_on P0) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). Proof. @@ -1682,7 +1680,6 @@ Definition gauge_fun_basis (b : set E) (h : open_nbhsbasis_convextvs b) := Definition seminorm_of := [set p : Norm.SemiNorm.type E | exists b (h : open_nbhsbasis_convextvs b), p = gauge_fun_basis h]. - Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E => -[/= b Bb _]. From 616d62ea01cc64577132dcc6c49748a661fba0c9 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 5 Nov 2026 15:43:44 +0100 Subject: [PATCH 08/18] clean --- theories/normedtype_theory/tvs.v | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 82034c6784..d79da44e30 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1876,7 +1876,6 @@ Qed. End generating_seminorm. - Section kernel. Context (R : realFieldType) (F : convexTvsType R). From 029a6c360ba66ed5fe08fc0e94aa5e316762a582 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 5 Nov 2026 16:26:00 +0100 Subject: [PATCH 09/18] Fail in line --- theories/functional_analysis/hahn_banach_theorem.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 6a7d1ac8f1..85f6a2a487 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -563,9 +563,11 @@ pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. rewrite Pg. suff -> : lcl xline = 1 by []. move/eqP: (xchooseP (line_linepred xline)). +(*have lem :(\val (xline)) = x by []. Fail rewrite lem.*) set xline':= (X in X =_ -> _); have -> : xline' = x by []. (*TODO weakness of line, to be understood *) -set x':= (X in X =_ -> _); rewrite -(scale1r x'). +(* Fail rewrite -(scale1r (x : V)). *) +set x':= (X in X =_ -> _). ; rewrite -(scale1r x'). move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. by apply: H. Qed. From b0dcf4c272b7e6d510111d76ca3611e19fac85ac Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Nov 2026 10:28:16 +0100 Subject: [PATCH 10/18] resolve line --- theories/functional_analysis/hahn_banach_theorem.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 85f6a2a487..9b9d6eed1d 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -563,11 +563,7 @@ pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. rewrite Pg. suff -> : lcl xline = 1 by []. move/eqP: (xchooseP (line_linepred xline)). -(*have lem :(\val (xline)) = x by []. Fail rewrite lem.*) -set xline':= (X in X =_ -> _); have -> : xline' = x by []. -(*TODO weakness of line, to be understood *) -(* Fail rewrite -(scale1r (x : V)). *) -set x':= (X in X =_ -> _). ; rewrite -(scale1r x'). +have {1}-> :(\val (xline)) = x by []; rewrite -{1}(scale1r (x : V)). move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. by apply: H. Qed. From d119f1da7e923c81ad35826fc7eb66878428a476 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 9 Nov 2026 17:34:26 +0900 Subject: [PATCH 11/18] Apply suggestion from @affeldt-aist --- theories/functional_analysis/hahn_banach_theorem.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 9b9d6eed1d..99eff4fc86 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -516,7 +516,7 @@ Proof. split; last first. (* proof in here is different than in the book - Jarchow mentions "a" continuous seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of -the set of seminorm generating the topology - its probably lacks an argument +the set of seminorms generating the topology - it probably lacks an argument saying that continuous seminorms are always bounded by this set of seminorms, which we haven't formalised here *) move => H. From 58b811edb41c283cb8181828156468d69cda54aa Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 9 Nov 2026 17:34:50 +0900 Subject: [PATCH 12/18] Apply suggestion from @affeldt-aist --- CHANGELOG_UNRELEASED.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 051d381010..432bfc0084 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -32,8 +32,6 @@ `pownMexpR_cvgr0`, `powRMexpR_cvgr0`, `pownMpowR_cvgr0`, `pownMexpr_cvgn0` + instance `is_derive1_powRl` -- in `ereal_normedtype.v`: - + lemma `ge0_cvgMly` ### Changed From 477de39f7dd451053dd0329583b1e7539fa8f0bc Mon Sep 17 00:00:00 2001 From: Marie Kerjean <43064157+mkerjean@users.noreply.github.com> Date: Mon, 9 Nov 2026 11:14:01 +0100 Subject: [PATCH 13/18] Apply suggestion from @affeldt-aist Co-authored-by: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> --- theories/functional_analysis/hahn_banach_theorem.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 99eff4fc86..6e279c2220 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -510,7 +510,7 @@ Qed. (*END TBA *) (* 7.2.3 in Jarchow *) -Lemma hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : +Corollary hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : (hausdorff_space V) <-> (forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l(x) != 0). Proof. split; last first. From 99f85eca3cf5664c0fabdeeff49c29e72873f550 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 9 Nov 2026 11:16:36 +0100 Subject: [PATCH 14/18] mention PR2166 --- theories/normedtype_theory/tvs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index d79da44e30..adfe84dfae 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -204,7 +204,7 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. - +(* TBD when PR#2166 is merged *) Lemma accessible_field (K : numFieldType) : accessible_space K^o. Proof. move=> x y xy. From 4f63d2ed657de4e94f5dd35f5f7cb7eb52cb99d9 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 9 Nov 2026 11:20:02 +0100 Subject: [PATCH 15/18] clean --- theories/functional_analysis/hahn_banach_theorem.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 6e279c2220..d3339dbaa6 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -495,16 +495,18 @@ Qed. End hahn_banach_extension_ctvs. (* TBA : to classical ? Where shoudl this go *) -Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). +Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : + a != 0 -> (t *: a = 0 -> t = 0). Proof. move=> a0 ta; apply: contrapT => /eqP t0. have : t^-1 *: (t *: a) = 0 by rewrite ta scaler0. by rewrite scalerA mulVf// scale1r; apply/eqP. Qed. -Lemma scaleIl (R : numFieldType) (V: lmodType R) (a : V) : a != 0 -> injective (fun t => t *: a). +Lemma scaleIl (R : numFieldType) (V: lmodType R) (a : V) : + a != 0 -> injective (fun t => t *: a). Proof. -move=> a0 s t => /eqP; rewrite -subr_eq0 -scalerBl => /eqP /(scaler_eq0 a0) /eqP. +move=> a0 s t => /eqP; rewrite -subr_eq0 -scalerBl=> /eqP /(scaler_eq0 a0) /eqP. by rewrite subr_eq0 => /eqP. Qed. (*END TBA *) From 9a5c52b71659f859ee890beb8f63e853757ed51e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Nov 2026 19:20:44 +0900 Subject: [PATCH 16/18] nitpick --- theories/normedtype_theory/tvs.v | 102 +++++++++--------- theories/topology_theory/topology_structure.v | 12 +-- 2 files changed, 56 insertions(+), 58 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index adfe84dfae..60ad3c5b67 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1877,73 +1877,71 @@ Qed. End generating_seminorm. Section kernel. -Context (R : realFieldType) (F : convexTvsType R). +Context {R : realFieldType} {F : convexTvsType R}. -(* Introduce a notation for kernels ?*) -Lemma continuous_closedkernel (f : {linear F -> R^o}): continuous f <-> closed (f @^-1` [set 0]). +(* TODO: Introduce a notation for kernels? *) +Lemma continuous_closedkernel (f : {linear F -> R^o}) : + continuous f <-> closed (f @^-1` [set 0]). Proof. split. move=> /continuous_closedP /(_ [set 0]); apply. - by apply: accessible_closed_set1; apply: accessible_field. -have []:= (eqVneq (f @^-1` [set 0]) [set : F]). - move => h _. - suff -> : f = (fun y=> 0) :> (F -> R) by apply: cst_continuous. + exact/accessible_closed_set1/accessible_field. +have [h _|] := eqVneq (f @^-1` [set 0]) [set: F]. + suff -> : f = (fun y=> 0) :> (F -> R) by exact: cst_continuous. apply: funext => x. - by have : [set : F] x by []; rewrite -h. -move=> s0 /closed_Ndense; move=> /(_ s0) /existsNP [U] /not_implyP [[x Ux]]. -move=> /not_implyP [oU] /forallNP /= Uf. -have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). -have /nbhsE0 [_ [V' /Bbasis [/= V BV VV'] VU]]: nbhs x U by rewrite nbhsE; exists U. -have [_ aV]: absolutely_convex_set V by apply: Bconv; rewrite inE. -have nfU: forall z, V z -> f z != f x. - move=> z Vz; apply/eqP => fzx. + by move/seteqP : h => [_ /(_ x)] ->. +move=> s0 /closed_Ndense => /(_ s0) /existsNP[/= U] /not_implyP[[x Ux]]. +move=> /not_implyP[oU] /forallNP /= Uf. +have [B Bconv [B0 Bbasis]] := @locally_convex _ F. +have /nbhsE0 [_ [V' /Bbasis [/= V BV VV'] VU]] : nbhs x U. + by rewrite nbhsE; exists U. +have [_ aV] : absolutely_convex_set V by exact/Bconv/mem_set. +have nfU z : V z -> f z != f x. + move=> Vz; apply/eqP => fzx. have Vnz : V (- z). - rewrite -scaleN1r; apply: aV; last by exists z => //. - by rewrite normrN normr1. - apply: Uf; split; first by apply: VU ; exists (-z); first by apply: VV'. + rewrite -scaleN1r; apply: (aV (- 1)); first by rewrite normrN1. + by exists z. + apply: Uf; split; first by apply: VU; exists (- z) => //; exact: VV'. by rewrite linearB; rewrite fzx subrr. -have [/=M fM]: exists M, forall z, V z -> `|f z | < M. - apply: contrapT; rewrite -forallNE /= => /(_ (`|f x|)) /existsNP [y]. - move=> /not_implyP [Vy] /negP; rewrite -leNgt => fxy. +have [/= M fM] : exists M, forall z, V z -> `|f z | < M. + apply: contrapT; rewrite -forallNE /= => /(_ `|f x|) /existsNP[y]. + move=> /not_implyP[Vy] /negP; rewrite -leNgt => fxy. have fy0 : f y != 0. - apply/eqP => fy0; move: fxy; rewrite fy0 normr0 normr_le0 => /eqP fx0. - by apply: (Uf x); split. - have Vyx : V ((`| f x|/ `| f y|) *: y). + apply/eqP; move: fxy => /[swap] ->; rewrite normr0 normr_le0 => /eqP fx0. + exact: (Uf x). + have Vyx : V ((`| f x | / `| f y |) *: y). apply: aV; last by exists y. - rewrite ger0_norm ?mulr_ge0 ?invr_ge0 //. - rewrite ler_pdivrMr ?mul1r // normr_gt0; apply/eqP => fy. - have := fxy; rewrite fy normr0 normr_le0 => /eqP fx0. - by apply: (Uf x); split. - have Vnyx : V ( - (`| f x|/ `| f y|) *: y). - apply: aV; last by exists ((`| f x|/ `| f y|) *: y); rewrite // scalerA -mulN1r. - by rewrite normrN normr1. - have [fxy0|fxy0|/eqP] := ltgtP 0 ((f x)/(f y)). + by rewrite ger0_norm ?divr_ge0// ler_pdivrMr ?mul1r// normr_gt0. + have Vnyx : V ( - (`| f x |/ `| f y |) *: y). + apply: (aV (- 1)); first by rewrite normrN1. + by exists ((`| f x |/ `| f y |) *: y) => //=; rewrite scaleN1r scaleNr. + have [fxy0|fxy0|/esym/eqP] := ltgtP 0 (f x / f y). - apply: (Uf ( x - (`|f x| / `|f y|) *: y)); split. - apply: VU; exists (- (`|f x| / `|f y|) *: y); first by apply: VV'. + apply: VU; exists (- (`|f x| / `|f y|) *: y); first exact: VV'. by rewrite scaleNr. - rewrite linearD linearN linearZ /=. - have -> : `|f x| / `|f y| = (f x)/(f y) by rewrite -normfV -normrM gtr0_norm. - by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. + rewrite linearD linearN linearZ/=. + have -> : `|f x| / `|f y| = f x / f y by rewrite -normfV -normrM gtr0_norm. + by rewrite -[X in _ - X]mulrAC -mulrA divff// mulr1 subrr. - apply: (Uf ( x + (`|f x| / `|f y|) *: y)); split. - by apply: VU; exists ((`|f x| / `|f y|) *: y); first by apply: VV'. - rewrite linearD linearZ /=. - have -> : `|f x| / `|f y| = - (f x)/(f y). + by apply: VU; exists ((`|f x| / `|f y|) *: y); first exact: VV'. + rewrite linearD linearZ/=. + have -> : `|f x| / `|f y| = - f x / f y. by rewrite -normfV -normrM ltr0_norm ?mulNr. by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. - - rewrite eq_sym mulf_eq0 => /orP [] /eqP. - by move=> fx0; apply: (Uf x); split. - by rewrite -invr0 => /invr_inj fyn0; move/eqP: fy0; apply. -have [M0|M0] := leP M 0 => //. - have := (fM 0); move => /(_ (nbhs_singleton _)); move=> /(_ (B0 V BV)). + - rewrite mulf_eq0 => /predU1P[dx0|]. + by apply: (Uf x); split. + by rewrite invr_eq0; exact/negP. +have [M0|M0] := leP M 0. + have /(_ (nbhs_singleton (B0 V BV))) := fM 0. by move=> /lt_le_trans /(_ M0); rewrite normr_lt0. -apply: continuousfor0_continuous => /= A; rewrite linear0 => -[r /= r0] rA. -have rM0 : r/ M != 0 by apply: lt0r_neq0; rewrite ?mulr_gt0 ?invr_gt0 //. -apply: (@filterS _ _ _ ( *:%R (r * M^-1) @` V)); last first. - by rewrite -(@scaler0 _ _ (r/M)); apply: nbhsZ; last by apply: B0. -move=> z /= [t] Vt <-; rewrite linearE /=; apply: rA => /=. -rewrite sub0r normrN -[_ *: _]/(_ * _) normrM -ltr_pdivlMl ?normr_gt0 //. -rewrite [in X in _ /= A; rewrite linear0 => -[r /= r0 rA]. +have rM0 : r / M != 0 by rewrite gt_eqF// divr_gt0. +apply: (@filterS _ _ _ ( *:%R (r * M^-1) @` V)); last first. + by rewrite -(@scaler0 _ _ (r / M)); apply: nbhsZ => //; exact: B0. +move=> z /= [t Vt <-]; rewrite linearE /=; apply: rA => /=. +rewrite sub0r normrN normrM -ltr_pdivlMl ?normr_gt0//. +rewrite [in X in _ < X]gtr0_norm ?divr_gt0//. +by rewrite invfM mulrAC mulVf ?gt_eqF// div1r invrK fM. Qed. End kernel. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 552abce1aa..08fbe6f5d6 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -1117,13 +1117,13 @@ apply/not_implyP; split; first exact: openT. by rewrite setTI => -[]. Qed. -Lemma closed_Ndense (T : topologicalType) (A : set T) : - (A != [set: T]) -> closed A -> ~ (dense A). +Lemma closed_Ndense {T : topologicalType} (A : set T) : + A != [set: T] -> closed A -> ~ dense A. Proof. -move=> /setTPn [t] nAt. -have A0: (~` A) !=set0 by exists t. -rewrite -openC => /[swap] /(_ _) /[swap] oA /(_ (~` A) A0 oA). -by move=> -[a [+ Aa]]; move=> /(_ Aa). +move=> AT. +have A0 : (~` A) !=set0 by apply/set0P; contra: AT; rewrite -setCT => /setC_inj. +rewrite -openC => /[swap] /(_ _) /[swap] oNA /(_ _ A0 oNA). +by rewrite setICl => /set0P; rewrite eqxx. Qed. Section basis. From f88b7062cc185f2a617696459dbbd3f985b1f46c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Nov 2026 20:16:44 +0900 Subject: [PATCH 17/18] linting --- theories/normedtype_theory/tvs.v | 93 ++++++++++++++++---------------- 1 file changed, 45 insertions(+), 48 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 60ad3c5b67..962ae388d0 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1305,59 +1305,57 @@ Qed. End openbasis. - +(**md This section shows that every convexTvsType admits a basis of closed + absolutely convex sets *) Section closedbasis. -(* This section shows that every convexTvsType admits a basis of closed -absolutely convex sets *) -Context (R : realFieldType) (E: convexTvsType R). +Context {R : realFieldType} {E : convexTvsType R}. Definition closed_nbhsbasis_ctvs := - [set closure b | b in (@nbhsbasis_convextvs R E)]. + [set closure b | b in @nbhsbasis_convextvs R E]. Lemma has_closed_nbhs_basis : nbhs_basis 0 closed_nbhsbasis_ctvs - /\ (forall b, closed_nbhsbasis_ctvs b -> (closed b /\ absolutely_convex_set b)). + /\ (forall b, closed_nbhsbasis_ctvs b -> closed b /\ absolutely_convex_set b). Proof. -have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +have [absconv [nbhs0 basis]] := svalP (cid2 (@locally_convex _ E)). split. - split; move=> /= a /=. - by move=> [b /nbhs0 nbhsb <-]; apply: filterS; first by apply: subset_closure. + split => /= a /=. + by move=> [b /nbhs0 nbhsb <-]; apply: filterS; first exact: subset_closure. move=> /nbhs0_add [b] /[dup] /basis [/= c nc cb]. move=> /closure_addset /subset_trans /[apply] cba. exists (closure c); first by exists c. - apply: subset_trans; last by exact: cba. - by apply: closureS. -move=> ? [c nc <-]; split; first by exact: closed_closure. + by apply: subset_trans cba; exact: closureS. +move=> ? [c nc <-]; split; first exact: closed_closure. have [convc balc] := absconv c (mem_set nc). split; rewrite /closure. - move => x y t; rewrite !inE /= => Bx By B. - move/nbhsE0 => [Bxy [b /basis [/= a /[dup ]/nbhs0 na0 na ab] aB]]. + move=> x y t; rewrite !inE /= => Bx By B. + move=> /nbhsE0[Bxy [b /basis [/= a /[dup ]/nbhs0 na0 na ab] aB]]. have [conva _] := absconv a (mem_set na). have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a) !=set0. apply: (Bx ([set x] `+ a)); rewrite nbhsE0; split. exists x => //=; exists 0; last by rewrite addr0. - by apply: nbhs_singleton. - exists a; first by apply: nbhs0. + exact: nbhs_singleton. + exists a; first exact: nbhs0. by move=> z /= [s sa <-]; exists x => //; exists s. have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a ) !=set0. apply: (By ([set y] `+ a )); rewrite nbhsE0; split. exists y => //=; exists 0; last by rewrite addr0. - by apply: nbhs_singleton => //=. - exists a ; first by apply: nbhs0. + exact: nbhs_singleton. + exists a ; first exact: nbhs0. by move=> // z /= [s sa <-]; exists y => //; exists s. exists (conv t (cx : convex_lmodType E) cy); split. - by apply/set_mem; apply: convc; rewrite !inE. + by apply/set_mem/convc; rewrite inE. apply: aB => /=; rewrite -acy -acx; exists (conv t (ax : convex_lmodType E) ay). - by apply: ab; apply/set_mem; apply: conva; rewrite !inE. + by apply: ab; apply/set_mem; apply: conva; rewrite inE. by rewrite addrACA -!scalerDr. move=> t t1 ? /= [x Bx] <- B. have [->|t0] := eqVneq t 0. - by rewrite scale0r => /nbhs_singleton B0; exists 0; split => //; apply: nbhs_singleton; apply: nbhs0. -move/(nbhsZ (invr_neq0 t0)); rewrite scalerA mulrC divff // scale1r. + rewrite scale0r => /nbhs_singleton B0; exists 0; split => //. + by apply: nbhs_singleton; exact: nbhs0. +move/(nbhsZ (invr_neq0 t0)); rewrite scalerA mulrC divff ?scale1r//. move/Bx => [z [cz [y by']]] /(congr1 (fun x => t *: x)). -rewrite scalerA divff // scale1r => ytz; exists y; split => //. -rewrite ytz; apply: balc; first by exact: t1. -by exists z. +rewrite scalerA divff ?scale1r// => ytz; exists y; split => //. +by rewrite ytz; apply: (balc _ t1); exists z. Qed. End closedbasis. @@ -1638,35 +1636,34 @@ exact: pshift0. Qed. Lemma hausdorff_seminorm_on : -hausdorff_space (seminorm_on P0) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). + hausdorff_space (seminorm_on P0) <-> + (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). Proof. split. - move/hausdorff_convextvs => H0 x; contra => HP. - have : forall p, P p -> p x = 0. - move=> p /HP /negP nlt0. - have:= (@norm_ge0 _ _ p x). - rewrite le0r; case; move/orP => []; first by move/eqP. - by move/nlt0 => //. - move => {HP} HP; apply: H0 => /= c [? [?]] [/= I IB] <- <- xic. - exists 0; split => //; apply: xic => /=; exists x => //; exists (-x); rewrite ?subrr //. - move=> i /= /IB /set_mem /= [p] /HP px0 [e e0] -> /=. - rewrite Theory.normN px0. - by apply: ballxx. -move=> H0; apply/hausdorff_convextvs => x /=; contra => /H0 [p Pp px0]. + move/hausdorff_convextvs => c0 x; contra => Px. + have {}Px : forall p, P p -> p x = 0. + move=> p /Px; rewrite -leNgt => px0. + by apply/eqP; rewrite eq_le px0//= norm_ge0. + apply: c0 => /= c [A1 [A2]] [/= I IB] <- <- xIc. + exists 0; split => //; apply: xIc => /=. + exists x => //; exists (- x);last by rewrite subrr. + move=> i /= /IB /set_mem /= [p] /Px px0 [e e0] -> /=. + by rewrite Theory.normN px0; exact: ballxx. +move=> neq0_P; apply/hausdorff_convextvs => x /=; contra => /neq0_P[p Pp px0]. exists (p @^-1` ball (p x) (p x)); last first. - by move=> /= ? ->; rewrite norm0 /ball /= subr0 ger0_norm ?norm_ge0 // ltxx. + by move=> /= _ ->; rewrite /ball/= norm0 subr0 gtr0_norm// ltxx. exists ([set x] `+ p @^-1` ball (0 : R) (p x)); last first. - move=> z /= [? -> [y + <-]]. - rewrite /ball /= sub0r normrN ger0_norm ?norm_ge0 // => pyx. - apply: le_lt_trans; first by apply: Theory.seminorm_normrB. + move=> z /= [_ -> [y + <-]]. + rewrite /ball /= sub0r normrN ger0_norm ?norm_ge0// => pyx. + apply: le_lt_trans; first exact: Theory.seminorm_normrB. by rewrite opprD addrA subrr sub0r Theory.normN. -exists (p @^-1` ball (0 : R) (p x)) => //. -exists ([fset (p @^-1` ball (0 : R) (p x))]%fset). - move=> ? ; rewrite inE => /eqP ->; apply/mem_set. - rewrite /seminorm_subbasis /=; exists p => //; exists (p x) => //. +exists (p @^-1` ball (0 : R) (p x)) => //=. +exists [fset (p @^-1` ball (0 : R) (p x))]%fset. + move=> _ /[!inE]/= ->. + by rewrite /seminorm_subbasis /=; exists p => //; exists (p x). apply/seteqP; split => z /=. - by rewrite /bigcap /= => /(_ (p @^-1` ball (0 : R) (p x))); apply; rewrite inE. -by move=> ballz => ? /=; rewrite inE => /eqP ->. + by move => /(_ (p @^-1` ball (0 : R) (p x)))/=; apply; rewrite inE. +by move=> ballz A/= /[!inE]/= ->. Qed. End convex_topology_seminorm. From 8a42c7b01346a616282095c63dfb5b57af38aa15 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Nov 2026 20:35:03 +0900 Subject: [PATCH 18/18] linting --- CHANGELOG_UNRELEASED.md | 2 +- .../functional_analysis/hahn_banach_theorem.v | 49 ++++++++++--------- .../pseudometric_normed_Zmodule.v | 30 ++++++------ theories/normedtype_theory/tvs.v | 34 ++++++------- 4 files changed, 57 insertions(+), 58 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 432bfc0084..d2f0a4a217 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,7 +12,7 @@ - in `tvs.v` + lemma `closure_convextvs`, `closure_addset` - + lemma ` accessible field` + + lemma `accessible field` + lemma `hausdorff_init_convextvs` + definition `closed_nbhsbasis_convextvs` + lemma `has_closed_nbhs_basis` diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index d3339dbaa6..b1e3cca42f 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -513,7 +513,8 @@ Qed. (* 7.2.3 in Jarchow *) Corollary hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : -(hausdorff_space V) <-> (forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l(x) != 0). + hausdorff_space V <-> + forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l x != 0. Proof. split; last first. (* proof in here is different than in the book - Jarchow mentions "a" continuous @@ -522,52 +523,52 @@ the set of seminorms generating the topology - it probably lacks an argument saying that continuous seminorms are always bounded by this set of seminorms, which we haven't formalised here *) move => H. - pose P := (@seminorm_of R V). - pose P0 := (@seminorm_ofneq0 R V). + pose P := @seminorm_of R V. + pose P0 := @seminorm_ofneq0 R V. suff : hausdorff_space (seminorm_on P0). - have [contVs _ ] := (@seminorm_convextvs _ V). - by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; apply: cs => //. + have [contVs _ ] := @seminorm_convextvs _ V. + by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; exact: cs. apply/hausdorff_seminorm_on=> x /H [l]. have [l0|l0|] := ltrgtP (l x) (0 : R) => //. - have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ (-1 *: l)). - exists p => //; apply: lt_le_trans; last by apply: lp. + have /linear_continuous_seminorm[p [sp _]/= lp] := + @continuous_fun _ _ (-1 *: l). + exists p => //; apply: lt_le_trans (lp _). by rewrite scaleN1r ltrNr oppr0. - have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ l). - by exists p => //; apply: lt_le_trans; last by apply: lp. + have /linear_continuous_seminorm[p [sp _] /= lp] := @continuous_fun _ _ l. + by exists p => //; exact: lt_le_trans (lp _). move=> haus x x0. -pose l := fun ( y : line x) => xchoose (line_linepred y). -have llinear: linear_for ( *:%R) l. - rewrite /l /= => t /= u v; apply: scaleIl; first by exact: x0. +pose l := fun y : line x => xchoose (line_linepred y). +have llinear : linear_for ( *:%R) l. + rewrite /l /= => t /= u v; apply: scaleIl; first exact: x0. rewrite scalerDl -scalerA. - move/eqP: (xchooseP (line_linepred u)) => <-. - move/eqP: (xchooseP (line_linepred v)) => <-. - move/eqP: (xchooseP (line_linepred (t *: u + v))) => <-. + move/eqP : (xchooseP (line_linepred u)) => <-. + move/eqP : (xchooseP (line_linepred v)) => <-. + move/eqP : (xchooseP (line_linepred (t *: u + v))) => <-. by rewrite (@GRing.valD _ _ (line x)) GRing.valZ. pose linlP := GRing.isLinear.Build _ _ _ _ l llinear. -pose linl : {linear ((init_subconvextvs (line x))) -> R^o} := HB.pack l linlP. +pose linl : {linear (init_subconvextvs (line x)) -> R^o} := HB.pack l linlP. have lcont : continuous linl. apply/continuous_closedkernel. - have -> : (linl @^-1` [set 0]) = [set 0]. + have -> : linl @^-1` [set 0] = [set 0]. apply/seteqP; split => u /=. - move/eqP: (xchooseP (line_linepred u)) => /[swap]; rewrite /l => ->. + move/eqP : (xchooseP (line_linepred u)) => /[swap]; rewrite /l => ->. by rewrite scale0r -(@GRing.val0 _ _ (line x)) => /val_inj. move=> u0; move/eqP: (xchooseP (line_linepred u)). rewrite u0 /= /l; move/eqP; rewrite eq_sym => /eqP. by move/(scaler_eq0 x0). apply: accessible_closed_set1; apply: hausdorff_accessible. - by apply: hausdorff_init_convextvs. + exact: hausdorff_init_convextvs. pose contlP := isContinuous.Build _ _ _ lcont. pose lcl : {linear_continuous (init_subconvextvs (line x)) -> R^o} := HB.pack (l : (init_subconvextvs (line x)) -> R^o) linlP contlP. have := (hahn_banach_extension_initialsubctvs lcl) => -[g Pg]; exists g. have xlinepred : (linepred x) x by apply/asboolP; exists 1; rewrite scale1r. -pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. +pose xline := exist (linepred x) _ xlinepred; have <- : \val xline = x by []. rewrite Pg. suff -> : lcl xline = 1 by []. -move/eqP: (xchooseP (line_linepred xline)). -have {1}-> :(\val (xline)) = x by []; rewrite -{1}(scale1r (x : V)). -move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. -by apply: H. +move/eqP : (xchooseP (line_linepred xline)). +have {1}-> : \val xline = x by []; rewrite -{1}(scale1r (x : V)). +by move/scaleIl => /(_ _)/esym; exact. Qed. (* TODO : more hahn banach separation theorems *) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index bbb9124ea4..d076b727de 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -266,27 +266,25 @@ Proof. move=> na. have := add_continuous 0 A. rewrite add0r => /(_ na) /= -[[b1 b2] /= [n1 n2] ba]. -exists (b1 `&` b2); first by apply: filterI. -by move => z /= [x [x1 _]] [y [_ y2]] <-; apply (ba (x,y)); split => /=. +exists (b1 `&` b2); first exact: filterI. +by move => z /= [x [x1 _]] [y [_ y2]] <-; exact: (ba (x, y)). Qed. -Lemma hausdorff_convextvs : (hausdorff_space M) <-> closed ([set 0 : M]). +Lemma hausdorff_convextvs : hausdorff_space M <-> closed [set 0 : M]. Proof. -split. - move=> /(_ (0:M)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. +split=> [|cl]. + move=> /(_ (0:M)) hF x /= cl; apply/esym/hF. move=> a b n0a /(cl b) [? [-> b0]]. - exists 0; split => //; exact: nbhs_singleton. -move => cl. -(* simpler proof using the closed subbasis ?*) -move=> x y H; apply: subr0_eq; have := H. -contra => xy0. -have nxy : nbhs (x-y) (~`[set 0]). - apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. - by apply/eqP. -have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). - by exact: sub_continuous. + by exists 0; split => //; exact: nbhs_singleton. +(* NB: simpler proof using the closed subbasis? *) +move=> x y H; apply: subr0_eq. +move: (H); contra => xy0. +have nxy : nbhs (x - y) (~` [set 0]). + by apply: open_nbhs_nbhs; split => /=; [exact: closed_openC|exact/eqP]. +have /(_ (~` [set 0]) nxy) [] : continuous_at (x, y) (fun z => z.1 - z.2). + exact: sub_continuous. move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. -by have := ab0 (z,z) => /=; rewrite subrr; apply. +by have := ab0 (z, z) => /=; rewrite subrr; exact. Qed. End TopologicalZmoduleTheory. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 962ae388d0..674421f205 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -402,23 +402,23 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U }. Section ConvexTvs_theory. -Context (R : numFieldType) (E : convexTvsType R). +Context {R : numFieldType} {E : convexTvsType R}. Lemma closure_convextvs (b : set E) : - closure b = \bigcap_(a in (nbhs (0 : E))) (b `+ a). + closure b = \bigcap_(a in nbhs (0 : E)) (b `+ a). Proof. -have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +have [absconv [] nbhs0 basis] := svalP (cid2 (@locally_convex _ E)). apply/seteqP; split => z H. move=> a' /basis [/=a /[dup] /mem_set /absconv [_ bala]]. move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. - exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. - by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. + exists y => //; exists (- t); last by apply/eqP; rewrite subr_eq zty. + by rewrite -scaleN1r; apply/aa'/(bala (- 1)); rewrite ?normrN1//=; exists t. move=> d; rewrite nbhsE0. -move => [dz] [/=a /basis [ /= a'/[dup] /mem_set /= /absconv [_ bala]]]. +move=> [dz] [/=a /basis [/= a'/[dup] /mem_set /= /absconv [_ bala]]]. move=> /nbhs0 /H [x bx [y ay]] xyz aa' zcd. -exists x; split => //; apply: zcd; exists (-y). - by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. -by apply: (addrI y); rewrite addrCA subrr addr0 addrC. +exists x; split => //; apply: zcd; exists (- y). + by rewrite -scaleN1r; apply/aa'/(bala (- 1)); rewrite ?normrN1//=; exists y. +by apply/eqP; rewrite subr_eq xyz. Qed. Lemma closure_addset (b : set E) : (nbhs 0 b) -> closure b `<=` b `+ b. @@ -430,7 +430,7 @@ Qed. End ConvexTvs_theory. Section SubLmodule_isSubConvexTvs. -Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). +Context {R : numFieldType} {V : convexTvsType R} (S : pred V) (U : subLmodType S). Definition init_subconvextvs := sub_initial_topology U. @@ -539,18 +539,18 @@ HB.instance Definition _ := @Uniform_isConvexTvs.Build R init_subconvextvs locally_convex_sub. HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. -Lemma hausdorff_init_convextvs : hausdorff_space V -> hausdorff_space init_subconvextvs. +Lemma hausdorff_init_convextvs : + hausdorff_space V -> hausdorff_space init_subconvextvs. Proof. move=> hV x y; rewrite /cluster /= /nbhs /= => cl. -apply: val_inj; apply: hV; rewrite nbhsE => A B /= [A' [oA Ax AA']]. +apply/val_inj/hV; rewrite nbhsE => A B /= [A' [oA Ax AA']]. rewrite nbhsE /= => -[B' [oB By BB']]. -have valA: nbhs_of_open (initial_open \val) x (\val @^-1` A'). - by rewrite /nbhs_of_open; exists (\val @^-1` A'); split => //=; exists A'. +have valA : nbhs_of_open (initial_open \val) x (\val @^-1` A'). + by exists (\val @^-1` A'); split => //=; exists A'. have : nbhs_of_open (initial_open \val) y (\val @^-1` B'). - by rewrite /nbhs_of_open; exists (\val @^-1` B'); split => //=; exists B'. + by exists (\val @^-1` B'); split => //=; exists B'. move/(cl (val @^-1` A') (val @^-1` B') valA) => [z /= [Az Bz]]; exists (val z). -split; first exact: AA'. -exact: BB'. +by split; [exact: AA'|exact: BB']. Qed. End SubLmodule_isSubConvexTvs.