分野別セミナー

凸集合は様々な数学的分野に現れ、凸関数や凸包の定義に使われる。 ベクトル集合における凸集合の抽象化として、重心の内在的公理化である 凸空間を定理証明支援系Coqで形式化した。凸空間はベクトル空間と 独立した概念（型）として定義される。これによって、凸空間上の関数が 定義しやすくなる。また、凸空間の錐空間への埋め込みを示す。その 埋め込みが計算的な性質を証明しやすくする。 この形式化を使い、凸空間のいくつかの公理化の等価性も証明している。 (Reynald Affeldt's(産業技術総合研究所), 才川隆文(名古屋大学)との共同研究)


※ 本講演は, 九州大学マス・フォア・イノベーション卓越大学院 マス・フォア・イノベーションセミナーとして実施されました.
cf. https://drive.google.com/file/d/1txRgTPcZqgxnodCIUe2NBP_I1eU7lyld/view