Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the $\textit{Number fields}$ section of the $\textit{L-functions and modular forms database}$ (LMFDB). These concern, for several number fields, the explicitly given $\textit{integral basis}$ of the ring of integers and the $\textit{discriminant}$. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.
The balanced incomplete block design (BIBD) problem is a difficult combinatorial problem with a large number of symmetries, which add complexity to its resolution. In this paper, we propose a dual (integer) problem representation that serves as an alternative to the classical binary formulation of the problem. We attack this problem incrementally: firstly, we propose basic algorithms (i.e. local search techniques and genetic algorithms) intended to work separately on the two different search spaces (i.e. binary and integer); secondly, we propose two hybrid schemes: an integrative approach (i.e. a memetic algorithm) and a collaborative model in which the previous methods work in parallel, occasionally exchanging information. Three distinct two-dimensional structures are proposed as communication topology among the algorithms involved in the collaborative model, as well as a number of migration and acceptance criteria for sending and receiving data. An empirical analysis comparing a large number of instances of our schemes (with algorithms possibly working on different search spaces and with/without symmetry breaking methods) shows that some of these algorithms can be considered the state of the art of the metaheuristic methods applied to finding BIBDs. Moreover, our cooperative proposal is a general scheme from which distinct algorithmic variants can be instantiated to handle symmetrical optimisation problems. For this reason, we have also analysed its key parameters, thereby providing general guidelines for the design of efficient/robust cooperative algorithms devised from our proposal.
If an algorithm is to be counted as a practically working solution to a decision problem, then the algorithm must must verifiable in some constructed and ``trusted'' theory such as PA or ZF. In this paper, a class of decision problems related to inconsistency proofs for a general class of formal theories is used to demonstrate that under this constructibility restriction, there are plausible arguments for the existence of decision problems which can be proved formally to be in NP, and for which there exists an explicitly constructible algorithm recognizing correct solutions in polynomial time, but for which there exists no explicitly constructible, verifiable solution algorithm. While these arguments do not solve the P versus NP problem in the classical sense of supplying a proof one way or the other in a ``trusted'' formal theory, arguably they resolve a constructive version of it.
In this paper we construct high order numerical methods for solving third and fourth orders nonlinear functional differential equations (FDE). They are based on the discretization of iterative methods on continuous level with the use of the trapezoidal quadrature formulas with corrections. Depending on the number of terms in the corrections we obtain methods of $O(h^4)$ and $O(h^6)$ accuracy. Some numerical experiments demonstrate the validity of the obtained theoretical results. The approach used here for the third and fourth orders nonlinear functional differential equations can be applied to functional differential equations of any orders.
We consider a nonlocal functional equation that is a generalization of the mathematical model used in behavioral sciences. The equation is built upon an operator that introduces a convex combination and a nonlinear mixing of the function arguments. We show that, provided some growth conditions of the coefficients, there exists a unique solution in the natural Lipschitz space. Furthermore, we prove that the regularity of the solution is inherited from the smoothness properties of the coefficients. As a natural numerical method to solve the general case, we consider the collocation scheme of piecewise linear functions. We prove that the method converges with the error bounded by the error of projecting the Lipschitz function onto the piecewise linear polynomial space. Moreover, provided sufficient regularity of the coefficients, the scheme is of the second order measured in the supremum norm. A series of numerical experiments verify the proved claims and show that the implementation is computationally cheap and exceeds the frequently used Picard iteration by orders of magnitude in the calculation time.
We propose a tamed-adaptive Milstein scheme for stochastic differential equations in which the first-order derivatives of the coefficients are locally H\"older continuous of order $\alpha$. We show that the scheme converges in the $L_2$-norm with a rate of $(1+\alpha)/2$ over both finite intervals $[0, T]$ and the infinite interval $(0, +\infty)$, under certain growth conditions on the coefficients.
Parameter inference for linear and non-Gaussian state space models is challenging because the likelihood function contains an intractable integral over the latent state variables. While Markov chain Monte Carlo (MCMC) methods provide exact samples from the posterior distribution as the number of samples go to infinity, they tend to have high computational cost, particularly for observations of a long time series. Variational Bayes (VB) methods are a useful alternative when inference with MCMC methods is computationally expensive. VB methods approximate the posterior density of the parameters by a simple and tractable distribution found through optimisation. In this paper, we propose a novel sequential variational Bayes approach that makes use of the Whittle likelihood for computationally efficient parameter inference in this class of state space models. Our algorithm, which we call Recursive Variational Gaussian Approximation with the Whittle Likelihood (R-VGA-Whittle), updates the variational parameters by processing data in the frequency domain. At each iteration, R-VGA-Whittle requires the gradient and Hessian of the Whittle log-likelihood, which are available in closed form for a wide class of models. Through several examples using a linear Gaussian state space model and a univariate/bivariate non-Gaussian stochastic volatility model, we show that R-VGA-Whittle provides good approximations to posterior distributions of the parameters and is very computationally efficient when compared to asymptotically exact methods such as Hamiltonian Monte Carlo.
In this paper we consider a class of conjugate discrete-time Riccati equations (CDARE), arising originally from the linear quadratic regulation problem for discrete-time antilinear systems. Recently, we have proved the existence of the maximal solution to the CDARE with a nonsingular control weighting matrix under the framework of the constructive method. Our contribution in the work is to finding another meaningful Hermitian solutions, which has received little attention in this topic. Moreover, we show that some extremal solutions cannot be attained at the same time, and almost (anti-)stabilizing solutions coincide with some extremal solutions. It is to be expected that our theoretical results presented in this paper will play an important role in the optimal control problems for discrete-time antilinear systems.
We present and analyze two stabilized finite element methods for solving numerically the Poisson--Nernst--Planck equations. The stabilization we consider is carried out by using a shock detector and a discrete graph Laplacian operator for the ion equations, whereas the discrete equation for the electric potential need not be stabilized. Discrete solutions stemmed from the first algorithm preserve both maximum and minimum discrete principles. For the second algorithm, its discrete solutions are conceived so that they hold discrete principles and obey an entropy law provided that an acuteness condition is imposed for meshes. Remarkably the latter is found to be unconditionally stable. We validate our methodology through numerical experiments.
In the framework of a mixed finite element method, a structure-preserving formulation for incompressible MHD equations with general boundary conditions is proposed. A leapfrog-type temporal scheme fully decouples the fluid part from the Maxwell part by means of staggered discrete time sequences and, in doing so, partially linearizes the system. Conservation and dissipation properties of the formulation before and after the decoupling are analyzed. We demonstrate optimal spatial and second-order temporal error convergence and conservation and dissipation properties of the proposed method using manufactured solutions, and apply it to the benchmark Orszag-Tang and lid-driven cavity test cases.
We propose a parametric hazard model obtained by enforcing positivity in the damped harmonic oscillator. The resulting model has closed-form hazard and cumulative hazard functions, facilitating likelihood and Bayesian inference on the parameters. We show that this model can capture a range of hazard shapes, such as increasing, decreasing, unimodal, bathtub, and oscillatory patterns, and characterize the tails of the corresponding survival function. We illustrate the use of this model in survival analysis using real data.