Module mathcomp.analysis.normedtype_theory.tvs

# Topological vector spaces This file introduces locally convex topological vector spaces. ``` NbhsNmodule == HB class, join of Nbhs and Nmodule NbhsZmodule == HB class, join of Nbhs and Zmodule NbhsLmodule K == HB class, join of Nbhs and Lmodule over K K is a numDomainType. PreTopologicalNmodule == HB class, join of Topological and Nmodule TopologicalNmodule == HB class, PreTopologicalNmodule with a continuous addition PreTopologicalZmodule == HB class, join of Topological and Zmodule topologicalZmodType == topological abelian group TopologicalZmodule == HB class, join of TopologicalNmodule and Zmodule with a continuous opposite operator preTopologicalLmodType K == topological space and Lmodule over K K is a numDomainType The HB class is PreTopologicalLmodule. topologicalLmodType K == topologicalNmodule and Lmodule over K with a continuous scaling operation The HB class is TopologicalLmodule. PreUniformNmodule == HB class, join of Uniform and Nmodule UniformNmodule == HB class, join of Uniform and Nmodule with a uniformly continuous addition PreUniformZmodule == HB class, join of Uniform and Zmodule UniformZmodule == HB class, join of UniformNmodule and Zmodule with uniformly continuous opposite operator PreUniformLmodule K == HB class, join of Uniform and Lmodule over K K is a numDomainType. UniformLmodule K == HB class, join of UniformNmodule and Lmodule with a uniformly continuous scaling operation K is a numFieldType. convexTvsType R == interface type for a locally convex tvs on a numDomain R A convex tvs is constructed over a uniform space. The HB class is ConvexTvs. subConvexTvsType R V S == join of subTopologicalType, convexTvsType, and subLmoduleType The HB class is SubConvexTvs. Instance: in particular, it is shown that a sub-Lmodule is a sub-convex TVS. PreTopologicalLmod_isConvexTvs == factory allowing the construction of a convex tvs from an Lmodule which is also a topological space {linear_continuous E -> F} == the type of all linear and continuous functions between E and F, where E is a NbhsLmodule.type and F a NbhsZmodule.type over a numDomainType R The HB class is called LinearContinuous. The notation {linear_continuous E -> F | s} also exists. lcfun E F s == membership predicate for linear continuous functions of type E -> F with scalar operator s : K -> F -> F E and F have type convexTvsType K. This is used in particular to attach a type of lmodType to {linear_continuous E -> F | s}. lcfun_spec f == specification for membership of the linear continuous function f ``` HB instances: - The type R^o (R : numFieldType) is endowed with the structure of ConvexTvs. - The product of two Tvs is endowed with the structure of ConvexTvs. - {linear_continuous E-> F} is endowed with a lmodType structure when E and F are convexTvs.