-
Constructing Optimal $L_{\infty}$ Star Discrepancy Sets
Authors:
François Clément,
Carola Doerr,
Kathrin Klamroth,
Luís Paquete
Abstract:
The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a very hard problem in the discrepancy community. Indeed, optimal point sets are, up to now, known only for $n\leq 6$ in dimension 2 and $n \leq 2$ for higher dimensions. We introduce in this paper mathematical pro…
▽ More
The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a very hard problem in the discrepancy community. Indeed, optimal point sets are, up to now, known only for $n\leq 6$ in dimension 2 and $n \leq 2$ for higher dimensions. We introduce in this paper mathematical programming formulations to construct point sets with as low $L_{\infty}$ star discrepancy as possible. Firstly, we present two models to construct optimal sets and show that there always exist optimal sets with the property that no two points share a coordinate. Then, we provide possible extensions of our models to other measures, such as the extreme and periodic discrepancies. For the $L_{\infty}$ star discrepancy, we are able to compute optimal point sets for up to 21 points in dimension 2 and for up to 8 points in dimension 3. For $d=2$ and $n\ge 7$ points, these point sets have around a 50% lower discrepancy than the current best point sets, and show a very different structure.
△ Less
Submitted 27 February, 2024; v1 submitted 29 November, 2023;
originally announced November 2023.
-
Heuristic Approaches to Obtain Low-Discrepancy Point Sets via Subset Selection
Authors:
François Clément,
Carola Doerr,
Luís Paquete
Abstract:
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While we prove that the heuristic does not necessarily return an optimal solution, we obtain very promising results for all teste…
▽ More
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While we prove that the heuristic does not necessarily return an optimal solution, we obtain very promising results for all tested dimensions. For example, for moderate point set sizes $30 \leq n \leq 240$ in dimension 6, we obtain point sets with $L_{\infty}$ star discrepancy up to 35% better than that of the first $n$ points of the Sobol' sequence. Our heuristic works in all dimensions, the main limitation being the precision of the discrepancy calculation algorithms.
We also provide a comparison with a recent energy functional introduced by Steinerberger [J. Complexity, 2019], showing that our heuristic performs better on all tested instances.
△ Less
Submitted 8 March, 2024; v1 submitted 27 June, 2023;
originally announced June 2023.
-
Partitions for stratified sampling
Authors:
Francois Clement,
Nathan Kirk,
Florian Pausinger
Abstract:
Classical jittered sampling partitions $[0,1]^d$ into $m^d$ cubes for a positive integer $m$ and randomly places a point inside each of them, providing a point set of size $N=m^d$ with small discrepancy. The aim of this note is to provide a construction of partitions that works for arbitrary $N$ and improves straight-forward constructions. We show how to construct equivolume partitions of the $d$-…
▽ More
Classical jittered sampling partitions $[0,1]^d$ into $m^d$ cubes for a positive integer $m$ and randomly places a point inside each of them, providing a point set of size $N=m^d$ with small discrepancy. The aim of this note is to provide a construction of partitions that works for arbitrary $N$ and improves straight-forward constructions. We show how to construct equivolume partitions of the $d$-dimensional unit cube with hyperplanes that are orthogonal to the main diagonal of the cube. We investigate the discrepancy of such point sets and optimise the expected discrepancy numerically by relaxing the equivolume constraint using different black-box optimisation techniques.
△ Less
Submitted 29 June, 2023; v1 submitted 20 April, 2022;
originally announced April 2022.
-
Lebesgue Induction and Tonelli's Theorem in Coq
Authors:
Sylvie Boldo,
François Clément,
Vincent Martin,
Micaela Mayero,
Houda Mouhcine
Abstract:
Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a…
▽ More
Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, ho** that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $σ$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.
△ Less
Submitted 10 February, 2022;
originally announced February 2022.
-
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.
-
Distribution of distances in five dimensions and related problems
Authors:
Francois Clement,
Thang Pham
Abstract:
In this paper, we study the Erdős-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $Δ(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we obtain stronger statements as follows:
If $|A|\gg p^{\frac{13}{22}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$
If…
▽ More
In this paper, we study the Erdős-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $Δ(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we obtain stronger statements as follows:
If $|A|\gg p^{\frac{13}{22}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$
If $|A|\gg p^{\frac{4}{7}}$, then $(A-A)^2+(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$
We also prove that if $p^{4/7}\ll |A-A|=K|A|\le p^{5/8}$, then \[|A^2+A^2|\gg \min \left\lbrace \frac{p}{K^4}, \frac{|A|^{8/3}}{K^{7/3}p^{2/3}}\right\rbrace.\] As a consequence, $|A^2+A^2|\gg p$ when $|A|\gg p^{5/8}$ and $K\sim 1$, where $A^2=\{x^2\colon x\in A\}$.
△ Less
Submitted 6 September, 2021; v1 submitted 29 April, 2021;
originally announced April 2021.
-
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
Authors:
Sylvie Boldo,
François Clément,
Florian Faissole,
Vincent Martin,
Micaela Mayero
Abstract:
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to exte…
▽ More
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $σ$-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou's lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of $L^p$~spaces such as Banach spaces.
△ Less
Submitted 9 December, 2021; v1 submitted 12 April, 2021;
originally announced April 2021.
-
Star Discrepancy Subset Selection: Problem Formulation and Efficient Approaches for Low Dimensions
Authors:
François Clèment,
Carola Doerr,
Luís Paquete
Abstract:
Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star discrepancy. First, we show that this problem is NP-hard. Then, we introduce a mixed integer linear formulation (MILP) and a combinatorial branch-and-bound (BB) algorithm for the star discrepancy subset selectio…
▽ More
Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star discrepancy. First, we show that this problem is NP-hard. Then, we introduce a mixed integer linear formulation (MILP) and a combinatorial branch-and-bound (BB) algorithm for the star discrepancy subset selection problem and we evaluate both approaches against random subset selection and a greedy construction on different use-cases in dimension two and three. Our results show that the MILP and BB are efficient in dimension two for large and small $m/n$ ratio, respectively, and for not too large n. However, the performance of both approaches decays strongly for larger dimensions and set sizes.
As a side effect of our empirical comparisons we obtain point sets of discrepancy values that are much smaller than those of common low-discrepancy sequences, random point sets, and of Latin Hypercube Sampling. This suggests that subset selection could be an interesting approach for generating point sets of small discrepancy value.
△ Less
Submitted 4 January, 2022; v1 submitted 19 January, 2021;
originally announced January 2021.
-
Lebesgue integration. Detailed proofs to be formalized in Coq
Authors:
François Clément,
Vincent Martin
Abstract:
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These funct…
▽ More
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.
△ Less
Submitted 2 April, 2021; v1 submitted 14 January, 2021;
originally announced January 2021.
-
Multiscale population dynamics in reproductive biology: singular perturbation reduction in deterministic and stochastic models
Authors:
Celine Bonnet,
Keltoum Chahour,
Frédérique Clément,
Marie Postel,
Romain Yvinec
Abstract:
In this study, we describe different modeling approaches for ovarian follicle population dynamics, based on either ordinary (ODE), partial (PDE) or stochastic (SDE) differential equations, and accounting for interactions between follicles. We put a special focus on representing the population-level feedback exerted by growing ovarian follicles onto the activation of quiescent follicles. We take ad…
▽ More
In this study, we describe different modeling approaches for ovarian follicle population dynamics, based on either ordinary (ODE), partial (PDE) or stochastic (SDE) differential equations, and accounting for interactions between follicles. We put a special focus on representing the population-level feedback exerted by growing ovarian follicles onto the activation of quiescent follicles. We take advantage of the timescale difference existing between the growth and activation processes to apply model reduction techniques in the framework of singular perturbations. We first study the linear versions of the models to derive theoretical results on the convergence to the limit models. In the nonlinear cases, we provide detailed numerical evidence of convergence to the limit behavior. We reproduce the main semi-quantitative features characterizing the ovarian follicle pool, namely a bimodal distribution of the whole population, and a slope break in the decay of the quiescent pool with aging.
△ Less
Submitted 4 March, 2019;
originally announced March 2019.
-
Stochastic nonlinear model for somatic cell population dynamics during ovarian follicle activation
Authors:
Frédérique Clément,
Frédérique Robin,
Romain Yvinec
Abstract:
In mammals, female germ cells are sheltered within somatic structures called ovarian follicles, which remain in a quiescent state until they get activated, all along reproductive life. We investigate the sequence of somatic cell events occurring just after follicle activation, starting by the awakening of precursor somatic cells, and their transformation into proliferative cells. We introduce a no…
▽ More
In mammals, female germ cells are sheltered within somatic structures called ovarian follicles, which remain in a quiescent state until they get activated, all along reproductive life. We investigate the sequence of somatic cell events occurring just after follicle activation, starting by the awakening of precursor somatic cells, and their transformation into proliferative cells. We introduce a nonlinear stochastic model accounting for the joint dynamics of the two cell types, and allowing us to investigate the potential impact of a feedback from proliferative cells onto precursor cells. To tackle the key issue of whether cell proliferation is concomitant or posterior to cell awakening, we assess both the time needed for all precursor cells to awake, and the corresponding increase in the total cell number with respect to the initial cell number. Using the probabilistic theory of first passage times, we design a numerical scheme based on a rigorous Finite State Projection and coupling techniques to compute the mean extinction time and the cell number at extinction time. We find that the feedback term clearly lowers the number of proliferative cells at the extinction time. We calibrate the model parameters using an exact likelihood approach. We carry out a comprehensive comparison between the initial model and a series of submodels, which helps to select the critical cell events taking place during activation, and suggests that awakening is prominent over proliferation.
△ Less
Submitted 9 December, 2020; v1 submitted 4 March, 2019;
originally announced March 2019.
-
Analysis and calibration of a linear model for structured cell populations with unidirectional motion : Application to the morphogenesis of ovarian follicles
Authors:
Frédérique Clément,
Frédérique Robin,
Romain Yvinec
Abstract:
We analyze a multi-type age dependent model for cell populations subject to unidirectional motion, in both a stochastic and deterministic framework. Cells are distributed into successive layers; they may divide and move irreversibly from one layer to the next. We adapt results on the large-time convergence of PDE systems and branching processes to our context, where the Perron-Frobenius or Krein-R…
▽ More
We analyze a multi-type age dependent model for cell populations subject to unidirectional motion, in both a stochastic and deterministic framework. Cells are distributed into successive layers; they may divide and move irreversibly from one layer to the next. We adapt results on the large-time convergence of PDE systems and branching processes to our context, where the Perron-Frobenius or Krein-Rutman theorem can not be applied. We derive explicit analytical formulas for the asymptotic cell number moments, and the stable age distribution. We illustrate these results numerically and we apply them to the study of the morphodynamics of ovarian follicles. We prove the structural parameter identifiability of our model in the case of age independent division rates. Using a set of experimental biological data, we estimate the model parameters to fit the changes in the cell numbers in each layer during the early stages of follicle development.
△ Less
Submitted 14 December, 2017;
originally announced December 2017.
-
The Lax-Milgram Theorem. A detailed proof to be formalized in Coq
Authors:
François Clément,
Vincent Martin
Abstract:
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The Lax-Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness…
▽ More
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The Lax-Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. The purpose of this document is to provide the formal proof community with a very detailed pen-and-paper proof of the Lax-Milgram theorem.
△ Less
Submitted 4 October, 2016; v1 submitted 13 July, 2016;
originally announced July 2016.
-
First-Order Indicators for the Estimation of Discrete Fractures in Porous Media
Authors:
Hend Ben Ameur,
Guy Chavent,
Cheikh Fatma,
François Clément,
Vincent Martin,
Jean E. Roberts
Abstract:
Faults and geological barriers can drastically affect the flow patterns in porous media. Such fractures can be modeled as interfaces that interact with the surrounding matrix. We propose a new technique for the estimation of the location and hydrogeological properties of a small number of large fractures in a porous medium from given distributed pressure or flow data. At each iteration, the algori…
▽ More
Faults and geological barriers can drastically affect the flow patterns in porous media. Such fractures can be modeled as interfaces that interact with the surrounding matrix. We propose a new technique for the estimation of the location and hydrogeological properties of a small number of large fractures in a porous medium from given distributed pressure or flow data. At each iteration, the algorithm builds a short list of candidates by comparing fracture indicators. These indicators quantify at the first order the decrease of a data misfit function; they are cheap to compute. Then, the best candidate is picked up by minimization of the objective function for each candidate. Optimally driven by the fit to the data, the approach has the great advantage of not requiring remeshing, nor shape derivation. The stability of the algorithm is shown on a series of numerical examples representative of typical situations.
△ Less
Submitted 21 October, 2016; v1 submitted 26 February, 2016;
originally announced February 2016.
-
Border collision bifurcations of stroboscopic maps in periodically driven spiking models
Authors:
Albert Granados,
Martin Krupa,
Frédérique Clément
Abstract:
In this work we consider a general non-autonomous hybrid system based on the integrate-and-fire model, widely used as simplified version of neuronal models and other types of excitable systems. Our unique assumption is that the system is monotonic, possesses an attracting subthreshold equilibrium point and is forced by means of periodic pulsatile (square wave) function.\\ In contrast to classical…
▽ More
In this work we consider a general non-autonomous hybrid system based on the integrate-and-fire model, widely used as simplified version of neuronal models and other types of excitable systems. Our unique assumption is that the system is monotonic, possesses an attracting subthreshold equilibrium point and is forced by means of periodic pulsatile (square wave) function.\\ In contrast to classical methods, in our approach we use the stroboscopic map (time-$T$ return map) instead of the so-called firing-map. It becomes a discontinuous map potentially defined in an infinite number of partitions. By applying theory for piecewise-smooth systems, we avoid relying on particular computations and we develop a novel approach that can be easily extended to systems with other topologies (expansive dynamics) and higher dimensions.\\ More precisely, we rigorously study the bifurcation structure in the two-dimensional parameter space formed by the amplitude and the duty cycle of the pulse. We show that it is covered by regions of existence of periodic orbits given by period adding structures. They do not only completely describe all the possible spiking asymptotic dynamics but also the behavior of the firing rate, which is a devil's staircase as a function of the parameters.
△ Less
Submitted 22 November, 2013; v1 submitted 3 October, 2013;
originally announced October 2013.
-
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program
Authors:
Sylvie Boldo,
François Clément,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis
Abstract:
Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing…
▽ More
Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.
△ Less
Submitted 2 June, 2014; v1 submitted 29 December, 2012;
originally announced December 2012.
-
Mixed-mode oscillations in a multiple time scale phantom bursting system
Authors:
Maciej Krupa,
Alexandre Vidal,
Mathieu Desroches,
Frédérique Clément
Abstract:
In this work we study mixed mode oscillations in a model of secretion of GnRH (Gonadotropin Releasing Hormone). The model is a phantom burster consisting of two feedforward coupled FitzHugh-Nagumo systems, with three time scales. The forcing system (Regulator) evolves on the slowest scale and acts by moving the slow nullcline of the forced system (Secretor). There are three modes of dynamics: puls…
▽ More
In this work we study mixed mode oscillations in a model of secretion of GnRH (Gonadotropin Releasing Hormone). The model is a phantom burster consisting of two feedforward coupled FitzHugh-Nagumo systems, with three time scales. The forcing system (Regulator) evolves on the slowest scale and acts by moving the slow nullcline of the forced system (Secretor). There are three modes of dynamics: pulsatility (transient relaxation oscillation), surge (quasi steady state) and small oscillations related to the passage of the slow nullcline through a fold point of the fast nullcline. We derive a variety of reductions, taking advantage of the mentioned features of the system. We obtain two results; one on the local dynamics near the fold in the parameter regime corresponding to the presence of small oscillations and the other on the global dynamics, more specifically on the existence of an attracting limit cycle. Our local result is a rigorous characterization of small canards and sectors of rotation in the case of folded node with an additional time scale, a feature allowing for a clear geometric argument. The global result gives the existence of an attracting unique limit cycle, which, in some parameter regimes, remains attracting and unique even during passages through a canard explosion.
△ Less
Submitted 13 February, 2012;
originally announced February 2012.
-
Optimal control of cell mass and maturity in a model of follicular ovulation
Authors:
Frédérique Clément,
Jean-Michel Coron,
Peipei Shang
Abstract:
In this paper, we study optimal control problems associated with a scalar hyperbolic conservation law modeling the development of ovarian follicles. Changes in the age and maturity of follicular cells are described by a 2D conservation law, where the control terms act on the velocities. The control problem consists in optimizing the follicular cell resources so that the follicular maturity reaches…
▽ More
In this paper, we study optimal control problems associated with a scalar hyperbolic conservation law modeling the development of ovarian follicles. Changes in the age and maturity of follicular cells are described by a 2D conservation law, where the control terms act on the velocities. The control problem consists in optimizing the follicular cell resources so that the follicular maturity reaches a maximal value in fixed time. Formulating the optimal control problem within a hybrid framework, we prove necessary optimality conditions in the form of Hybrid Maximum Principle. Then we derive the optimal strategy and show that there exists at least one optimal bang-bang control with one single switching time.
△ Less
Submitted 15 October, 2012; v1 submitted 9 February, 2012;
originally announced February 2012.
-
DynPeak : An algorithm for pulse detection and frequency analysis in hormonal time series
Authors:
Alexandre Vidal,
Qinghua Zhang,
Claire Médigue,
Stéphane Fabre,
Frédérique Clément
Abstract:
The endocrine control of the reproductive function is often studied from the analysis of luteinizing hormone (LH) pulsatile secretion by the pituitary gland. Whereas measurements in the cavernous sinus cumulate anatomical and technical difficulties, LH levels can be easily assessed from jugular blood. However, plasma levels result from a convolution process due to clearance effects when LH enters…
▽ More
The endocrine control of the reproductive function is often studied from the analysis of luteinizing hormone (LH) pulsatile secretion by the pituitary gland. Whereas measurements in the cavernous sinus cumulate anatomical and technical difficulties, LH levels can be easily assessed from jugular blood. However, plasma levels result from a convolution process due to clearance effects when LH enters the general circulation. Simultaneous measurements comparing LH levels in the cavernous sinus and jugular blood have revealed clear differences in the pulse shape, the amplitude and the baseline. Besides, experimental sampling occurs at a relatively low frequency (typically every 10 min) with respect to LH highest frequency release (one pulse per hour) and the resulting LH measurements are noised by both experimental and assay errors. As a result, the pattern of plasma LH may be not so clearly pulsatile. Yet, reliable information on the InterPulse Intervals (IPI) is a prerequisite to study precisely the steroid feedback exerted on the pituitary level. Hence, there is a real need for robust IPI detection algorithms. In this article, we present an algorithm for the monitoring of LH pulse frequency, basing ourselves both on the available endocrinological knowledge on LH pulse (shape and duration with respect to the frequency regime) and synthetic LH data generated by a simple model. We make use of synthetic data to make clear some basic notions underlying our algorithmic choices. We focus on explaining how the process of sampling affects drastically the original pattern of secretion, and especially the amplitude of the detectable pulses. We then describe the algorithm in details and perform it on different sets of both synthetic and experimental LH time series. We further comment on how to diagnose possible outliers from the series of IPIs which is the main output of the algorithm.
△ Less
Submitted 22 December, 2011;
originally announced December 2011.
-
Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
Authors:
Sylvie Boldo,
Francois Clement,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis
Abstract:
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to g…
▽ More
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.
△ Less
Submitted 12 July, 2012; v1 submitted 8 December, 2011;
originally announced December 2011.
-
Image Segmentation with Multidimensional Refinement Indicators
Authors:
Hend Ben Ameur,
Guy Chavent,
Francois Clément,
Pierre Weis
Abstract:
We transpose an optimal control technique to the image segmentation problem. The idea is to consider image segmentation as a parameter estimation problem. The parameter to estimate is the color of the pixels of the image. We use the adaptive parameterization technique which builds iteratively an optimal representation of the parameter into uniform regions that form a partition of the domain, hence…
▽ More
We transpose an optimal control technique to the image segmentation problem. The idea is to consider image segmentation as a parameter estimation problem. The parameter to estimate is the color of the pixels of the image. We use the adaptive parameterization technique which builds iteratively an optimal representation of the parameter into uniform regions that form a partition of the domain, hence corresponding to a segmentation of the image. We minimize an error function during the iterations, and the partition of the image into regions is optimally driven by the gradient of this error. The resulting segmentation algorithm inherits desirable properties from its optimal control origin: soundness, robustness, and flexibility.
△ Less
Submitted 23 May, 2011; v1 submitted 10 November, 2010;
originally announced November 2010.
-
Formal Proof of a Wave Equation Resolution Scheme: the Method Error
Authors:
Sylvie Boldo,
François Clément,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis
Abstract:
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs.…
▽ More
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.
△ Less
Submitted 14 November, 2011; v1 submitted 5 May, 2010;
originally announced May 2010.
-
Formal Proof of a Wave Equation Resolution Scheme: the Method Error
Authors:
Sylvie Boldo,
François Clément,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis
Abstract:
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs.…
▽ More
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.
△ Less
Submitted 9 November, 2011; v1 submitted 27 January, 2010;
originally announced January 2010.
-
Endogenous circannual rhythm in LH secretion: insight from signal analysis coupled with mathematical modelling
Authors:
Alexandre Vidal,
Claire Médigue,
Benoit Malpaux,
Frédérique Clément
Abstract:
In sheep as in many vertebrates, the seasonal pattern of reproduction is timed by the annual photoperiodic cycle, characterized by seasonal changes in the daylength. The photoperiodic information is translated into a circadian profile of melatonin secretion. After multiple neuronal relays (within the hypothalamus), melatonin impacts GnRH (gonadotrophin releasing hormone) secretion that in turn c…
▽ More
In sheep as in many vertebrates, the seasonal pattern of reproduction is timed by the annual photoperiodic cycle, characterized by seasonal changes in the daylength. The photoperiodic information is translated into a circadian profile of melatonin secretion. After multiple neuronal relays (within the hypothalamus), melatonin impacts GnRH (gonadotrophin releasing hormone) secretion that in turn controls ovarian cyclicity. The pattern of GnRH secretion is mirrored into that of LH (luteinizing hormone) secretion, whose plasmatic level can be easily measured. We addressed the question of whether there exists an endogenous circannual rhythm in a tropical sheep population that exhibits clear seasonal ovarian activity when ewes are subjected to temperate latitudes. We based our analysis on LH time series collected in the course of 3 years from ewes subjected to a constant photoperiodic regime. Due to intra- and inter- animal variability and unequal sampling times, the existence of an endogenous rhythm is not straightforward. We have used time-frequency signal processing methods to extract hidden rhythms from the data. To further investigate the LF (low frequency) and HF (high frequency) components of the signals, we have designed a mathematical model of LH plasmatic level accounting for the effect of experimental sampling times. The model enables us to confirm the existence of an endogenous circannual rhythm, to investigate the action mechanism of photoperiod on the pulsatile pattern of LH secretion (control of the interpulse interval) and to conclude that the HF component is mainly due to the experimental sampling protocol.
△ Less
Submitted 10 March, 2009;
originally announced March 2009.
-
Bifurcation-based parameter tuning in a model of the GnRH pulse and surge generator
Authors:
Frédérique Clément,
Alexandre Vidal
Abstract:
We investigate a model of the GnRH pulse and surge generator, with the definite aim of constraining the model GnRH output with respect to a physiologically relevant list of specifications. The alternating pulse and surge pattern of secretion results from the interaction between a GnRH secreting system and a regulating system exhibiting fast-slow dynamics. The mechanisms underlying the behavior o…
▽ More
We investigate a model of the GnRH pulse and surge generator, with the definite aim of constraining the model GnRH output with respect to a physiologically relevant list of specifications. The alternating pulse and surge pattern of secretion results from the interaction between a GnRH secreting system and a regulating system exhibiting fast-slow dynamics. The mechanisms underlying the behavior of the model are reminded from the study of the Boundary-Layer System according to the "dissection method" principle. Using singular perturbation theory, we describe the sequence of bifurcations undergone by the regulating (FitzHugh-Nagumo) system, encompassing the rarely investigated case of homoclinic connexion. Basing on pure dynamical considerations, we restrict the space of parameter search for the regulating system and describe a foliation of this restricted space, whose leaves define constant duration ratios between the surge and the pulsatility phase in the whole system. We propose an algorithm to fix the parameter values to also meet the other prescribed ratios dealing with amplitude and frequency features of the secretion signal. We finally apply these results to illustrate the dynamics of GnRH secretion in the ovine species and the rhesus monkey.
△ Less
Submitted 10 September, 2008;
originally announced September 2008.
-
Multi-scale modeling of follicular ovulation as a reachability problem
Authors:
Nki Echenim,
Frederique Clement,
Michel Sorine
Abstract:
During each ovarian cycle, only a definite number of follicles ovulate, while the others undergo a degeneration process called atresia. We have designed a multi-scale mathematical model where ovulation and atresia result from a hormonal controlled selection process. A 2D-conservation law describes the age and maturity structuration of the follicular cell population. In this paper, we focus on th…
▽ More
During each ovarian cycle, only a definite number of follicles ovulate, while the others undergo a degeneration process called atresia. We have designed a multi-scale mathematical model where ovulation and atresia result from a hormonal controlled selection process. A 2D-conservation law describes the age and maturity structuration of the follicular cell population. In this paper, we focus on the operating mode of the control, through the study of the characteristics of the conservation law. We describe in particular the set of microscopic initial conditions leading to the macroscopic phenomenon of either ovulation or atresia, in the framework of backwards reachable sets theory.
△ Less
Submitted 6 February, 2007; v1 submitted 20 July, 2006;
originally announced July 2006.
-
The Multi-Dimensional Refinement Indicators Algorithm for Optimal Parameterization
Authors:
Hend Ben Ameur,
François Clément,
Pierre Weis,
Guy Chavent
Abstract:
The estimation of distributed parameters in partial differential equations (PDE) from measures of the solution of the PDE may lead to under-determination problems. The choice of a parameterization is a usual way of adding a-priori information by reducing the number of unknowns according to the physics of the problem. The refinement indicators algorithm provides a fruitful adaptive parameterizati…
▽ More
The estimation of distributed parameters in partial differential equations (PDE) from measures of the solution of the PDE may lead to under-determination problems. The choice of a parameterization is a usual way of adding a-priori information by reducing the number of unknowns according to the physics of the problem. The refinement indicators algorithm provides a fruitful adaptive parameterization technique that parsimoniously opens the degrees of freedom in an iterative way. We present a new general form of the refinement indicators algorithm that is applicable to the estimation of multi-dimensional parameters in any PDE. In the linear case, we state the relationship between the refinement indicator and the decrease of the usual least-squares data misfit objective function. We give numerical results in the simple case of the identity model, and this application reveals the refinement indicators algorithm as an image segmentation technique.
△ Less
Submitted 16 January, 2008; v1 submitted 29 June, 2006;
originally announced June 2006.
-
Mathematical modeling of the GnRH pulse and surge generator
Authors:
Frederique Clement,
Jean-Pierre Francoise
Abstract:
We propose a mathematical model allowing for the alternating pulse and surge pattern of GnRH (Gonadotropin Releasing Hormone) secretion. The model is based on the coupling between two systems running on different time scales. The faster system corresponds to the average activity of GnRH neurons, while the slower one corresponds to the average activity of regulatory neurons. The analysis of the s…
▽ More
We propose a mathematical model allowing for the alternating pulse and surge pattern of GnRH (Gonadotropin Releasing Hormone) secretion. The model is based on the coupling between two systems running on different time scales. The faster system corresponds to the average activity of GnRH neurons, while the slower one corresponds to the average activity of regulatory neurons. The analysis of the slow/fast dynamics exhibited within and between both systems allows to explain the different patterns (slow oscillations, fast oscillations and periodical surge) of GnRH secretion. Specifications on the model parameter values are derived from physiological knowledge in terms of amplitude, frequency and plateau length of oscillations. The behavior of the model is finally illustrated by numerical simulations reproducing natural ovarian cycles and either direct or indirect actions of ovarian steroids on GnRH secretion.
△ Less
Submitted 27 October, 2006; v1 submitted 15 November, 2005;
originally announced November 2005.
