arXiv subjects

Joseph K. Miller

Publications and source records attributed to Joseph K. Miller.

7 recordsLinked to original sources

arXiv2026

A Formalization of the Mean-Field Derivation of the Vlasov Equation

We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone. Reuse is a second check, by a definition we introduce: whether the development yields a self-contained layer of general mathematics the wider library could absorb. The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route -- existence, uniqueness, the stability estimate and mean-field limit, and a short-window superposition principle (weak solutions are Lagrangian). The human's role was to direct, not to write proofs: to scope the definitions, steer the decompositions, and triage the library's gaps; the AI agent executed. The formalization certifies the proof of each statement as written; whether the written statement is the intended theorem stays the mathematician's judgment. The optimal-transport machinery that fell out of the build (in particular, properties of the Wasserstein-1 metric and the Kantorovich-Rubinstein duality theorem) separates into a self-contained layer that compiles against Mathlib alone: about a sixth of the development (49 of 299 declarations), behind a 22-declaration interface with no reverse dependency. The headline theorems ran in about a week, the full development in about a month. We report the quantitative claims as observations of one game, not as general laws. The game's rules name no particular system, so the methodological framing is meant to outlast the tools of any one run.

cs.AI↗

arXiv2025

Emergence of fermion-mediated interactions in Bose-Fermi mixtures

This work is inspired by recent experimental observations in ultracold atomic Bose-Fermi mixtures [DeSalvo et al., Nature 568 (2019)]. These experiments reveal the emergence of an attractive fermion-mediated interaction between bosons, as well as a stability-instability transition. We give the first mathematical demonstration of this transition by studying the low-energy spectrum of a many-body interspecies Hamiltonian. More precisely, we show the convergence of its eigenvalues towards those of an effective Bose Hamiltonian, which includes fermion-mediated effects. Applying this result to a model with short-range potentials, we derive a stability-instability transition in the bosonic subsystem, driven by the Bose-Fermi coupling strength $g$. For small $|g|$, the bosons form a stable Bose-Einstein condensate with the energy per particle uniformly bounded from below. For large $|g|$, the energy per particle is no longer uniformly bounded from below, signaling the collapse of the condensate.

math-ph↗

arXiv2025

On the effective dynamics of Bose-Fermi mixtures

In this work, we describe the dynamics of a Bose-Einstein condensate interacting with a degenerate Fermi gas, at zero temperature. First, we analyze the mean-field approximation of the many-body Schrödinger dynamics and prove emergence of a coupled Hartree-type system of equations. We obtain rigorous error control that yields a non-trivial scaling window in which the approximation is meaningful. Second, starting from this Hartree system, we identify a novel scaling regime in which the fermion distribution behaves semi-clasically, but the boson field remains quantum-mechanical; this is one of the main contributions of the present article. In this regime, the bosons are much lighter and more numerous than the fermions. We then prove convergence to a coupled Vlasov-Hartee system of equations with an explicit convergence rate.

math-ph↗

arXiv2024

Inhomogeneous wave kinetic equation and its hierarchy in polynomially weighted $L^\infty$ spaces

Inspired by ideas stemming from the analysis of the Boltzmann equation, in this paper we expand well-posedness theory of the spatially inhomogeneous 4-wave kinetic equation, and also analyze an infinite hierarchy of PDE associated with this nonlinear equation. More precisely, we show global in time well-posedness of the spatially inhomogeneous 4-wave kinetic equation for polynomially decaying initial data. For the associated infinite hierarchy, we construct global in time solutions using the solutions of the wave kinetic equation and the Hewitt-Savage theorem. Uniqueness of these solutions is proved by using a combinatorial board game argument tailored to this context, which allows us to control the factorial growth of the Dyson series.

math.AP↗

arXiv2024

On the global in time existence and uniqueness of solutions to the Boltzmann hierarchy

In this paper we establish the global in time existence and uniqueness of solutions to the Boltzmann hierarchy, a hierarchy of equations instrumental for the rigorous derivation of the Boltzmann equation from many particles. Inspired by available $L^{\infty}$-based a-priori estimate for solutions to the Boltzmann equation, we develop the polynomially weighted $L^\infty$ a-priori bounds for solutions to the Boltzmann hierarchy and handle the factorial growth of the number of terms in the Dyson's series by reorganizing the sum through a combinatorial technique known as the Klainerman-Machedon board game argument. This paper is the first work that exploits such a combinatorial technique in conjunction with an $L^{\infty}$-based estimate to prove uniqueness of the mild solutions to the Boltzmann hierarchy. Our proof of existence of global in time mild solutions to the Boltzmann hierarchy for admissible initial data is constructive and it employs known global in time solutions to the Boltzmann equation via a Hewitt-Savage type theorem.

math.AP↗

arXiv2022

A rigorous derivation of the Hamiltonian structure for the Vlasov equation

We consider the Vlasov equation in any spatial dimension, which has long been known to be an infinite-dimensional Hamiltonian system whose bracket structure is of Lie-Poisson type. In parallel, it is classical that the Vlasov equation is a mean-field limit for a pairwise interacting Newtonian system. Motivated by this knowledge, we provide a rigorous derivation of the Hamiltonian structure of the Vlasov equation, both the Hamiltonian functional and Poisson bracket, directly from the many-body problem. One may view this work as a classical counterpart to arXiv:1908.03847, which provided a rigorous derivation of the Hamiltonian structure of the cubic nonlinear Schrödinger equation from the many-body problem for interacting bosons in a certain infinite particle number limit, the first result of its kind. In particular, our work settles a question of Marsden, Morrison, and Weinstein on providing a "statistical basis" for the bracket structure of the Vlasov equation.

math.AP↗

arXiv2021

A Rigorous Derivation of a Boltzmann System for a Mixture of Hard-Sphere Gases

In this paper, we rigorously derive a Boltzmann equation for mixtures from the many body dynamics of two types of hard sphere gases. We prove that the microscopic dynamics of two gases with different masses and diameters is well defined, and introduce the concept of a two parameter BBGKY hierarchy to handle the non-symmetric interaction of these gases. As a corollary of the derivation, we prove Boltzmann's propagation of chaos assumption for the case of a mixtures of gases.

math.AP↗