论文标题
凸面和圆锥形空间中的正式冒险
Formal Adventures in Convex and Conical Spaces
论文作者
论文摘要
凸集集中在各种数学理论中出现，用于定义诸如凸函数和船体之类的概念。作为从矢量空间中凸集的常规定义的抽象，我们基于将点的手术进行操作，在coq中正式化了凸集集合的内在公理化，即凸空间。凸空间对应于不指周围矢量空间的特定类型。这简化了功能上的定义。我们显示了应用程序，包括在分布类型上定义的信息理论功能的凸度。我们还展示了如何将凸空间嵌入到抽象的真实锥体中，并使用嵌入作为缓解计算的有效装置。
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets in vector spaces, we formalize in Coq an intrinsic axiomatization of convex sets, namely convex spaces, based on an operation taking barycenters of points. A convex space corresponds to a specific type that does not refer to a surrounding vector space. This simplifies the definitions of functions on it. We show applications including the convexity of information-theoretic functions defined over types of distributions. We also show how convex spaces are embedded in conical spaces, which are abstract real cones, and use the embedding as an effective device to ease calculations.
