Seminorm tvs

CHANGELOG_UNRELEASED.md

@@ -248,6 +248,43 @@
   + definition `preimage_set_system`
   + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
     `preimage_set_system_id`
+- in `functions.v`:
+  + lemmas `linfunP`, `linfun_eqP`
+  + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
+
+- in `tvs.v`:
+  + structure `LinearContinuous`
+  + factory `isLinearContinuous`
+  + instance of `ChoiceType` on `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the scalar multiplication of a function of type
+    `LinearContinuous`
+  + instance of `Continuous` on \-f when f is of type `LinearContinuous`
+  + instance of `SubModClosed` on `{linear_continuous _ -> _}`
+  + instance of `SubLModule` on  `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` on the null function
+  + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
+  + definitions `lcfun`, `lcfun_key, `lcfunP`
+  + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
+   `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
+  + lemmas `lcfun_continuous` and `lcfun_linear`
+
+  + ...
+- in `derive.v`:
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+  + lemmas `derivable0`, `derive0`, `is_derive0`
+- in `topology_structure.v`:
+  + lemma `not_limit_pointE`
+
+- in `separation_axioms.v`:
+  + lemmas `limit_point_closed`
+- in `convex.v`:
+  + lemma `convex_setW`
+- in `convex.v`:
+  + lemma `convexW`
+
+### Changed
 
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
@@ -354,6 +391,31 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- in set_interval.v
+  + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + structure `SubNormedZmodule`, notation `subNormedZmodType`
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+### Changed
+
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+
+- moved from `topology_structure.v` to `filter.v`:
+  + lemma `continuous_comp` (and generalized)
+
+- in `numfun.v`:
+  + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
+  + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
+  + `funeD_posD` renamed to `funeDB` and direction of the equality changed
+
 ### Renamed
 
 - in `tvs.v`:

CHANGELOG_UNRELEASED_new.md

@@ -0,0 +1,52 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge)
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+- in `filter.v`:
+  + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+
+- in `topology_structure.v`:
+  + structure `SubTopological`, notation `subTopologicalType`
+
+- in `tvs.v`:
+  + structure `SubConvexTvs`, notation `subConvexTvsType`
+
+- in `normed_module.v`:
+  + structure `SubNormedModule`, notation `subNormedModType`
+  + instance `ent_xsection_filter`
+  + factory `SubLmodule_isSubNormedmodule`
+
+- new file `hahn_banach_theorem.v`:
+  + module `LinearGraph`
+    * definitions `graph`, `linear_graph`
+    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
+  + module `HahnBanachZorn`
+    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
+    * record `zorn_type`
+    * definition `zphi`
+    * lemma `zorn_type_eq`
+    * definition `zornS`
+    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
+  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
+
+### Deprecated
+
+### Renamed
+
+### Generalized
+
+### Removed
+
+
+
+

classical/unstable.v

@@ -671,7 +671,27 @@ Proof.
 by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD.
 Qed.
 
+Lemma distC (v w : L) : norm (v - w) = norm (w - v).
+Proof.
+by rewrite -(normN (v - w)) opprB.
+Qed.
+
 End Theory.
+
+Section realTheory.
+Variables (K : realDomainType) (L : lmodType K) (norm : SemiNorm.type L).
+
+Lemma seminorm_normrB x y: `|norm x - norm y| <= norm (x - y).
+Proof.
+have [pxy | pyx] := leP (norm x) (norm y).
+  rewrite ler0_norm ?subr_le0 // opprB.
+  rewrite lerBlDl; rewrite  -(@normN _ _ norm (x-y)) opprB.
+  by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
+rewrite gtr0_norm ?subr_gt0 // lerBlDl.
+by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
+Qed.
+
+End realTheory.
 End Theory.
 
 Module Import Exports. HB.reexport. End Exports.

theories/normedtype_theory/normed_module.v

@@ -132,7 +132,7 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
+Lemma ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
 Proof.
 apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
@@ -145,16 +145,29 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
 by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
+#[local] Lemma ball_balanced_set (r : K) : balanced_set (ball (0 : V) r).
+Proof.
+move => t /= t1 z /= [y].
+rewrite -ball_normE /= !sub0r !normrN => + <-.
+rewrite normrZ.
+case: (eqVneq `|t| (1 : K)).
+  by move=> -> ; rewrite mul1r.
+move=> t11.
+have : (`|t| <1) by rewrite lt_neqAle; apply/andP; split.
+by move => lt1 yr; rewrite -[ltRHS]mul1r ltr_pM ?normr_ge0.
+Qed.
+
 (** NB: we have almost the same proof in `tvs.v` *)
 Let locally_convex_set :
   exists2 B : set_system (convex_lmodType V),
-    (forall b, b \in B -> convex_set b) & basis B.
+    (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B.
 Proof.
-exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
-  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set.
-split; first by move=> B [x] [r] ->; exact: ball_open.
-move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
-by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
+exists [set B | exists2 r, 0 < r &  B = ball 0 r].
+  move=> b; rewrite inE /= => -[r _ ->]; split; first by exact: ball_convex_set.
+  by exact: ball_balanced_set.
+split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx.
+move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=.
+by exists (ball 0 r)=> //; exists r.
 Qed.
 
 HB.instance Definition _ :=
@@ -2012,10 +2025,6 @@ rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//.
 by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0.
 Unshelve. all: by end_near. Qed.
 
-Lemma continuousfor0_continuous (f : {linear V -> W}) :
-  {for 0, continuous f} -> continuous f.
-Proof. by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed.
-
 Lemma linear_bounded_continuous (f : {linear V -> W}) :
   bounded_near f (nbhs 0) <-> continuous f.
 Proof.