Showing 1–3 of 3 results for author: Leclerc, L

Two equivalent descriptions of opetopes: in terms of zoom complexes and of partial orders

Authors: Louise Leclerc

Abstract: We introduce in this paper a definition of (non necessarily positive) opetopes where faces are organised in a poset. Then we show that this description is equivalent to that given in terms of constellations by Kock, Joyal, Batanin and Mascari. We introduce in this paper a definition of (non necessarily positive) opetopes where faces are organised in a poset. Then we show that this description is equivalent to that given in terms of constellations by Kock, Joyal, Batanin and Mascari. △ Less

Submitted 4 September, 2024; originally announced September 2024.

MSC Class: 06A75; 18N99

A poset-like approach to positive opetopes

Authors: Louise Leclerc

Abstract: We introduce in this paper a new formalisation of positive opetopes where faces are organised in a poset. Then we show that our definition is equivalent to that of positives opetopes as given by Marek Zawadowski. We introduce in this paper a new formalisation of positive opetopes where faces are organised in a poset. Then we show that our definition is equivalent to that of positives opetopes as given by Marek Zawadowski. △ Less

Submitted 28 May, 2024; originally announced May 2024.

MSC Class: 06A06; 06A07 ACM Class: G.2

A Coq Formalization of the Bochner integral

Authors: Sylvie Boldo, François Clément, Louise Leclerc

Abstract: The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a depen… ▽ More The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions. △ Less

Submitted 10 February, 2022; v1 submitted 10 January, 2022; originally announced January 2022.