Seminorm tvs

CHANGELOG_UNRELEASED.md

@@ -173,6 +173,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)
@@ -226,6 +263,31 @@
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
 
+- 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

@@ -647,7 +647,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.