Regularity of solutions of Vlasov-Maxwell equations

### What is the conjecture

The Vlasov-Maxwell system describes the evolution of a collisionless plasma, coupling a kinetic transport equation with Maxwell's equations. Let $f(t, x, v)$ denote the distribution function on phase space (position $x \in \mathbb{R}^3$, velocity $v \in \mathbb{R}^3$), and let $\mathbf{E}(t, x)$ and $\mathbf{B}(t, x)$ be the electric and magnetic fields. The system is:

$$\frac{\partial f}{\partial t} + v \cdot \nabla_x f + (e/m)(\mathbf{E} + v \times \mathbf{B}) \cdot \nabla_v f = 0$$

$$\nabla \times \mathbf{E} = -\frac{\partial \mathbf{B}}{\partial t}, \quad \nabla \times \mathbf{B} = \mu_0 \mathbf{J} + \mu_0 \epsilon_0 \frac{\partial \mathbf{E}}{\partial t}$$

where the current density is $\mathbf{J}(t, x) = e \int v f(t, x, v) \, dv$ and $e, m, \mu_0, \epsilon_0$ are physical constants.

The regularity conjecture asks: For what initial conditions (on $f_0(x, v)$ and electromagnetic fields) do classical (smooth) solutions exist globally in time? What is the optimal regularity of weak solutions, and how does the velocity averaging lemma facilitate the regularity theory?

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.oca.eu/images/LAGRANGE/pages_perso/nbesse/pub/NBesse_jhde18.pdf, https://arxiv.org/pdf/2203.01615, https://projecteuclid.org/journals/communications-in-mathematical-sciences/volume-2/issue-2/Global-Weak-Solutions-to-the-RelativisticVlasov-Maxwell-System-Revisited/cms/1109706532.pdf, https://projecteuclid.org/journals/communications-in-mathematical-physics/volume-154/issue-2/Global-weak-solutions-of-the-Vlasov-Maxwell-system-with-boundary/cmp/1104252970.pdf, https://en.wikipedia.org/wiki/Vlasov_equation

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-03-08)

Building blocks (1-3; from search results):
- Partial differential equations (Mathlib has PDE solvers, function spaces)
- Maxwell equations (standard electromagnetic field theory)
- Measure theory and integration on phase space

Missing pieces (exactly 2; unclear/absent from search results):
- Kinetic theory formalism: transport equations on phase space with velocity-dependent coupling
- Vlasov-Maxwell specific infrastructure: formalization of the kinetic-electromagnetic coupling and velocity averaging lemma

Rating justification (1-2 sentences): While Mathlib provides strong support for PDEs and function spaces, there is no existing formalization of kinetic theory or the Vlasov-Maxwell system itself. Stating the conjecture requires significant development of phase space transport equation theory and its coupling with Maxwell equations, though the foundational mathematical objects (PDEs, measures, function spaces) exist.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-35
* ams-82
* ams-78

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

No repository file, test, or entry point is identified. Start by reading the linked papers and checking the repository's existing formalized conjectures; completion would require stating the Vlasov-Maxwell regularity conjecture in Lean, including the missing kinetic-theory and coupling infrastructure described in the issue.

Written by the indexing model from the issue text.