Derivation of the Vlasov equation from N-particle Hamiltonian dynamics

Formalization of the companion paper (vlasov.tex). This file develops the mean-field theory of the Vlasov equation:

• the N-particle mean-field Hamiltonian and Newton equations of motion;
• the empirical measure of a configuration and its weak (distributional) evolution along Newton trajectories;
• the distributional Vlasov equation and its Lagrangian (characteristic-flow) formulation;
• the Kantorovich–Rubinstein convolution estimate and the Dobrushin Wasserstein-1 stability estimate;
• the mean-field limit theorem: the empirical measures of the N-particle system converge in W₁ to the Vlasov solution as N → ∞.

(tex: …) labels cross-reference the companion LaTeX paper.

Basic type aliases and notation

Throughout, d : ℕ is the spatial dimension and N : ℕ is the number of particles. Phase space for a single particle is EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d).

§1 Equation (Hamiltonian) (tex: eq:HN)

noncomputable def Vlasov.hamiltonianN {d : ℕ} (N : ℕ) (W : PhysSpace d → ℝ) (X V : Fin N → PhysSpace d) : ℝ

(tex: eq:HN) The mean-field Hamiltonian for N identical unit-mass particles in ℝ^d:

H_N(X, V) = Σ_{i=1}^{N} |v_i|² / 2 + (1/N) Σ_{1 ≤ i < j ≤ N} W(x_i − x_j).

The factor 1/N normalises the interaction energy so that kinetic and potential energies are of the same order as N → ∞.

Equations

• Vlasov.hamiltonianN N W X V = ∑ i : Fin N, ‖V i‖ ^ 2 / 2 + 1 / ↑N * ∑ i : Fin N, ∑ j : Fin N, if ↑i < ↑j then W (X i - X j) else 0

§2 Equation (Hamilton / Newton equations of motion) (tex: eq:newton)

def Vlasov.IsNewtonSolution {d : ℕ} (N : ℕ) (gradW : PhysSpace d → PhysSpace d) (X V : ℝ → Fin N → PhysSpace d) : Prop

(tex: eq:newton) Predicate asserting that a curve (X, V) : ℝ → (Fin N → PhysSpace d)² satisfies the N-particle mean-field Newton equations

x'_i = v_i, v'i = −(1/N) Σ{j ≠ i} ∇W(x_i − x_j), i = 1, …, N.

gradW is the gradient ∇W : ℝ^d → ℝ^d of the pair potential.

Equations

• One or more equations did not get rendered due to their size.

§3 Assumption (tex: ass:W)

class Vlasov.AssW {d : ℕ} (W : PhysSpace d → ℝ) : Prop

(tex: ass:W) Standing assumption on the pair potential W : ℝ^d → ℝ.

W belongs to C^{1,1}(ℝ^d): it is differentiable with a globally Lipschitz gradient. Additionally W is even: W(−x) = W(x) for all x. The Lipschitz constant L := Lip(∇W) is finite.

• differentiable : Differentiable ℝ W

  W is continuously differentiable.

• even (x : PhysSpace d) : W (-x) = W x

  W is even.

• lipschitzGrad : ∃ (L : NNReal), LipschitzWith L fun (x : PhysSpace d) => fderiv ℝ W x

  The gradient ∇W is Lipschitz with some constant L ≥ 0.

class Vlasov.AssW2 {d : ℕ} (W : PhysSpace d → ℝ) extends Vlasov.AssW W : Prop

(tex: ass:W2) Strengthened standing assumption for the weak ⟹ Lagrangian bridge: AssW (so W ∈ C^{1,1}, i.e. ∇W globally Lipschitz, and W even) together with ∇W ∈ C¹ (so W ∈ C²).

The extra gradContDiff field is stated on fun x => fderiv ℝ W x — the same object as AssW.lipschitzGrad — so the C^{1,1} (Lipschitz) and C² (continuously differentiable) facts concern one map. This is what makes the Vlasov phase-space field C¹ in space, which the characteristic flow's C¹ dependence on its initial point (the variational equation) requires.

Only the weak ⟹ Lagrangian bridge (LeanPool/Vlasov/OT/WeakToLagrangian.lean) carries AssW2; the marquee vlasovWellPosedness / dobrushin stay at the weaker AssW (arbitrary Lipschitz constant).

• differentiable : Differentiable ℝ W
• even (x : PhysSpace d) : W (-x) = W x
• lipschitzGrad : ∃ (L : NNReal), LipschitzWith L fun (x : PhysSpace d) => fderiv ℝ W x
• gradContDiff : ContDiff ℝ 1 fun (x : PhysSpace d) => fderiv ℝ W x

  ∇W is continuously differentiable (equivalently W ∈ C²).

theorem Vlasov.assW_zero {d : ℕ} : AssW fun (x : PhysSpace d) => 0

The zero potential satisfies the standing assumption ass:W — a machine-checked witness that the hypothesis class AssW is non-vacuous (interaction-free transport is an admissible instance of every headline theorem).

theorem Vlasov.assW2_zero {d : ℕ} : AssW2 fun (x : PhysSpace d) => 0

The zero potential satisfies the strengthened assumption ass:W2 — a machine-checked witness that AssW2 (and hence the hypothesis class of the weak ⟹ Lagrangian bridge) is non-vacuous.

theorem Vlasov.gradient_zero_of_even {d : ℕ} (W : PhysSpace d → ℝ) [hW : AssW W] : gradient W 0 = 0

Helper: under [AssW W] (even + differentiable), the gradient of W at the origin vanishes.

Mathematical content: differentiating W(-x) = W(x) at x = 0 and using HasFDerivAt.unique gives fderiv W 0 = -fderiv W 0, hence gradient W 0 = -gradient W 0. In the real vector space EuclideanSpace ℝ (Fin d) this forces gradient W 0 = 0.

Used by empiricalMeasureSolvesVlasov (cor:empirical-vlasov) to kill the diagonal correction term in weakEvolutionEmpiricalMeasure.

§4 Definition (Empirical measure) (tex: def:empirical)

noncomputable def Vlasov.empiricalMeasure {d : ℕ} (N : ℕ) (X V : Fin N → PhysSpace d) : MeasureTheory.Measure (PhaseSpace d)

(tex: def:empirical) The empirical measure of a configuration (X, V) ∈ (ℝ^d × ℝ^d)^N:

μ^N[X, V] := (1/N) Σ_{i=1}^{N} δ_{(X_i, V_i)}.

Returns a MeasureTheory.Measure (PhaseSpace d). It is a probability measure when N ≥ 1.

Equations

• Vlasov.empiricalMeasure N X V = (1 / ↑N) • ∑ i : Fin N, MeasureTheory.Measure.dirac (X i, V i)

theorem Vlasov.empiricalMeasure_isProbabilityMeasure {d : ℕ} (N : ℕ) [NeZero N] (X V : Fin N → PhysSpace d) : MeasureTheory.IsProbabilityMeasure (empiricalMeasure N X V)

(tex: def:empirical) When N ≥ 1 the empirical measure is a probability measure.

Proof: μ(univ) = (1/N) · Σᵢ δ_{zᵢ}(univ) = (1/N) · N · 1 = 1, where each Dirac mass evaluates to 1 on the universal set via the Measure.dirac.isProbabilityMeasure instance.

noncomputable def Vlasov.empiricalMeasureCurve {d : ℕ} (N : ℕ) (X V : ℝ → Fin N → PhysSpace d) : ℝ → MeasureTheory.Measure (PhaseSpace d)

(tex: def:empirical) The time-dependent empirical measure μ_t^N along a solution of eq:newton.

Equations

• Vlasov.empiricalMeasureCurve N X V t = Vlasov.empiricalMeasure N (X t) (V t)

§5 Proposition (Weak evolution of the empirical measure) (tex: prop:weak)

noncomputable def Vlasov.convolveFunctionMeasure {d : ℕ} (k : PhysSpace d → PhysSpace d) (ρ : MeasureTheory.Measure (PhysSpace d)) (x : PhysSpace d) : PhysSpace d

Convolution of a function k : ℝ^d → ℝ^d with a (finite) measure ρ on ℝ^d: (k * ρ)(x) := ∫ k(x − y) dρ(y).

Equations

• Vlasov.convolveFunctionMeasure k ρ x = ∫ (y : Vlasov.PhysSpace d), k (x - y) ∂ρ

noncomputable def Vlasov.spatialMarginal {d : ℕ} (μ : MeasureTheory.Measure (PhaseSpace d)) : MeasureTheory.Measure (PhysSpace d)

Spatial marginal of a measure on phase space.

Equations

• Vlasov.spatialMarginal μ = MeasureTheory.Measure.map Prod.fst μ

theorem Vlasov.empiricalMeasure_integral_eq {d : ℕ} (N : ℕ) (X V : Fin N → PhysSpace d) (φ : PhaseSpace d → ℝ) : ∫ (z : PhaseSpace d), φ z ∂empiricalMeasure N X V = 1 / ↑N * ∑ i : Fin N, φ (X i, V i)

The integral of a function φ against the empirical measure empiricalMeasure N X V equals (1/N) * ∑ i, φ(X i, V i), by unfolding the weighted sum of Dirac masses.

theorem Vlasov.hasDerivAt_phi_along_trajectory {d : ℕ} (N : ℕ) (X V : ℝ → Fin N → PhysSpace d) (hX : ∀ (t : ℝ) (i : Fin N), HasDerivAt (fun (t : ℝ) => X t i) (V t i) t) (a : ℝ → Fin N → PhysSpace d) (hV : ∀ (t : ℝ) (i : Fin N), HasDerivAt (fun (t : ℝ) => V t i) (a t i) t) (φ : PhaseSpace d → ℝ) (φ' : PhaseSpace d → PhaseSpace d →L[ℝ] ℝ) (hφ_fderiv : ∀ (z : PhaseSpace d), HasFDerivAt φ (φ' z) z) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (hgradXφ : ∀ (z : PhaseSpace d), gradXφ z = gradient (fun (x : PhysSpace d) => φ (x, z.2)) z.1) (hgradVφ : ∀ (z : PhaseSpace d), gradVφ z = gradient (fun (v : PhysSpace d) => φ (z.1, v)) z.2) (t : ℝ) (i : Fin N) : HasDerivAt (fun (s : ℝ) => φ (X s i, V s i)) (inner ℝ (V t i) (gradXφ (X t i, V t i)) + inner ℝ (a t i) (gradVφ (X t i, V t i))) t

For a smooth test function φ, the chain rule gives: the map t ↦ φ(X t i, V t i) has derivative ⟨V t i, gradXφ (X t i, V t i)⟩ + ⟨a t i, gradVφ (X t i, V t i)⟩ at t, where a t i is the acceleration vector at particle i and time t.

φ's Fréchet derivative is an input hypothesis hφ_fderiv rather than derived inside the helper, keeping the body a straight composition: · HasDerivAt.prodMk hX hV gives the curve derivative t ↦ (X t i, V t i). · (hφ_fderiv (X t i, V t i)).comp_hasDerivAt composes through φ. · Unfolding gradXφ/gradVφ via hgradXφ/hgradVφ and rewriting the Fréchet derivative's action via inner-product partial-derivative identities gives the target inner-product form.

theorem Vlasov.hasDerivAt_empiricalIntegral_sum {d : ℕ} (N : ℕ) (gradW : PhysSpace d → PhysSpace d) (X V : ℝ → Fin N → PhysSpace d) (hSol : IsNewtonSolution N gradW X V) (φ : PhaseSpace d → ℝ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (hgradXφ : ∀ (z : PhaseSpace d), gradXφ z = gradient (fun (x : PhysSpace d) => φ (x, z.2)) z.1) (hgradVφ : ∀ (z : PhaseSpace d), gradVφ z = gradient (fun (v : PhysSpace d) => φ (z.1, v)) z.2) (t : ℝ) : HasDerivAt (fun (s : ℝ) => ∫ (z : PhaseSpace d), φ z ∂empiricalMeasureCurve N X V s) (1 / ↑N * ∑ i : Fin N, (inner ℝ (V t i) (gradXφ (X t i, V t i)) + inner ℝ (-(1 / ↑N) • ∑ j : Fin N, if j ≠ i then gradW (X t i - X t j) else 0) (gradVφ (X t i, V t i)))) t

The derivative of t ↦ ∫ φ d(empiricalMeasureCurve N X V t) equals the finite sum expression (1/N) * Σᵢ [⟨V t i, gradXφ (X t i, V t i)⟩ + ⟨aᵢ, gradVφ (X t i, V t i)⟩] where aᵢ = -(1/N) Σ_{j≠i} gradW(X t i - X t j) is the Newton acceleration, obtained by combining empiricalMeasure_integral_eq and hasDerivAt_phi_along_trajectory with HasDerivAt.sum and HasDerivAt.const_smul.

theorem Vlasov.convolveFunctionMeasure_empiricalSpatial_eq {d : ℕ} (N : ℕ) (gradW : PhysSpace d → PhysSpace d) (hgradW_meas : Measurable gradW) (X V : ℝ → Fin N → PhysSpace d) (t : ℝ) (i : Fin N) : convolveFunctionMeasure gradW (spatialMarginal (empiricalMeasureCurve N X V t)) (X t i) = (1 / ↑N) • ∑ j : Fin N, gradW (X t i - X t j)

Convolution of the kernel gradW against the spatial marginal ofthe empirical measure unfolds to the explicit finite sum (1/N) • Σⱼ gradW(X t i − X t j). This separates the measure-pushforward / Dirac-integration machinery from the algebraic "add and subtract the diagonal" step in diagonalCorrection_eq.

Proof strategy:

1. empiricalMeasureCurve and empiricalMeasure unfold to (1/N : ℝ≥0∞) • Σⱼ Measure.dirac (X t j, V t j).
2. Measure.map_smul (MeasureTheory/Measure/Map.lean:127) pushes Prod.fst through the scalar.
3. Measure.map_add (MeasureTheory/Measure/Map.lean:103) + finset induction distributes Prod.fst over the sum, giving (1/N : ℝ≥0∞) • Σⱼ Measure.dirac (X t j).
4. convolveFunctionMeasure unfolds to ∫ y, gradW(X t i − y) ∂ρ.
5. integral_smul_measure (Bochner) extracts the (1/N).toReal = 1/N scalar; integral_finsetSum_measure (Integral/Bochner/Basic.lean) distributes integration over the finite sum of Diracs; integral_dirac' (Integral/Bochner/Basic.lean) collapses each summand to gradW(X t i − X t j).

theorem Vlasov.diagonalCorrection_eq {d : ℕ} (N : ℕ) (gradW : PhysSpace d → PhysSpace d) (hgradW_meas : Measurable gradW) (X V : ℝ → Fin N → PhysSpace d) (gradVφ : PhaseSpace d → PhysSpace d) (t : ℝ) : 1 / ↑N * ∑ i : Fin N, inner ℝ (-(1 / ↑N) • ∑ j : Fin N, if j ≠ i then gradW (X t i - X t j) else 0) (gradVφ (X t i, V t i)) = -(1 / ↑N) * ∑ i : Fin N, inner ℝ (convolveFunctionMeasure gradW (spatialMarginal (empiricalMeasureCurve N X V t)) (X t i)) (gradVφ (X t i, V t i)) + 1 / ↑N ^ 2 * ∑ i : Fin N, inner ℝ (gradW 0) (gradVφ (X t i, V t i))

The remainder term r in the weak evolution identity equals (1/N²) * Σᵢ ⟨gradW 0, gradVφ(X t i, V t i)⟩: this is the diagonal correction obtained when extending the Newton-equation sum Σ_{j≠i} to all j (the diagonal j = i summand contributes gradW(X t i - X t i) = gradW 0).

This lemma is pure inner-product algebra atop convolveFunctionMeasure_empiricalSpatial_eq: extend Σ_{j≠i} to Σⱼ via Finset.sum_ite_ne or Finset.sum_compl_add_sum, distribute the inner product with inner_sub_left/inner_smul_left, recognise the (1/N) • Σⱼ gradW factor as the convolveFunctionMeasure unfolding.

theorem Vlasov.diagonalCorrection_bound {d : ℕ} (N : ℕ) [NeZero N] (gradW : PhysSpace d → PhysSpace d) (X V : ℝ → Fin N → PhysSpace d) (gradVφ : PhaseSpace d → PhysSpace d) (hgradW_bdd : BddAbove (Set.range fun (x : PhysSpace d) => ‖gradW x‖)) (hgradVφ_bdd : BddAbove (Set.range fun (z : PhaseSpace d) => ‖gradVφ z‖)) (t : ℝ) : |1 / ↑N ^ 2 * ∑ i : Fin N, inner ℝ (gradW 0) (gradVφ (X t i, V t i))| ≤ 1 / ↑N * ⨆ (x : PhysSpace d), ‖gradW x‖ * ⨆ (z : PhaseSpace d), ‖gradVφ z‖

The remainder bound: for the diagonal correction r = (1/N²) * Σᵢ⟨gradW 0, gradVφ(zᵢ)⟩, we have |r| ≤ (1/N) * (⨆ x, ‖gradW x‖) * (⨆ z, ‖gradVφ z‖), using abs_inner_le_norm on each summand and the fact that the sum has N terms.

The two BddAbove hypotheses are essential: ciSup over an unbounded function returns junk value 0 on ℝ, which would make the inequality false in the unbounded case. The .tex's ‖∇W‖_∞ ‖∇_v φ‖_∞ implicitly assumes L^∞ boundedness; making it explicit here keeps the lemma honest. (For gradVφ: it comes from ∇_v φ of a smooth compactly supported φ, so the bound is a consequence of HasCompactSupport — but expressing that derivation requires Mathlib API that's awkward to assemble; easier to pass the bound as a hypothesis.)

theorem Vlasov.weakEvolutionEmpiricalMeasure_hasDerivAt {d : ℕ} (N : ℕ) (W : PhysSpace d → ℝ) [AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (X V : ℝ → Fin N → PhysSpace d) (hSol : IsNewtonSolution N gradW X V) (φ : PhaseSpace d → ℝ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (hgradXφ : ∀ (z : PhaseSpace d), gradXφ z = gradient (fun (x : PhysSpace d) => φ (x, z.2)) z.1) (hgradVφ : ∀ (z : PhaseSpace d), gradVφ z = gradient (fun (v : PhysSpace d) => φ (z.1, v)) z.2) (t : ℝ) : HasDerivAt (fun (s : ℝ) => ∫ (z : PhaseSpace d), φ z ∂empiricalMeasureCurve N X V s) (∫ (z : PhaseSpace d), inner ℝ z.2 (gradXφ z) - inner ℝ (convolveFunctionMeasure gradW (spatialMarginal (empiricalMeasureCurve N X V t)) z.1) (gradVφ z) ∂empiricalMeasureCurve N X V t + 1 / ↑N ^ 2 * ∑ i : Fin N, inner ℝ (gradW 0) (gradVφ (X t i, V t i))) t

Derivative-identity core of prop:weak, without the L^∞ boundedness hypotheses. Along a Newton solution the map t ↦ ⟨μ_t^N, φ⟩ is differentiable, with derivative the Vlasov pairing plus the explicit diagonal correction (1/N²) Σᵢ ⟨∇W(0), ∇_v φ(zᵢ)⟩. The BddAbove hypotheses of weakEvolutionEmpiricalMeasure feed only its quantitative (1/N)‖∇W‖_∞‖∇_vφ‖_∞ bound conjunct, not this identity — keeping them out here is what lets empiricalMeasureSolvesVlasov (and the packaged empiricalMeasure_isVlasovSolution) run hypothesis-free beyond ass:W.

theorem Vlasov.weakEvolutionEmpiricalMeasure {d : ℕ} (N : ℕ) [NeZero N] (W : PhysSpace d → ℝ) [AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (X V : ℝ → Fin N → PhysSpace d) (hSol : IsNewtonSolution N gradW X V) (φ : PhaseSpace d → ℝ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (_hφ_compact : HasCompactSupport φ) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (hgradXφ : ∀ (z : PhaseSpace d), gradXφ z = gradient (fun (x : PhysSpace d) => φ (x, z.2)) z.1) (hgradVφ : ∀ (z : PhaseSpace d), gradVφ z = gradient (fun (v : PhysSpace d) => φ (z.1, v)) z.2) (hgradW_bdd : BddAbove (Set.range fun (x : PhysSpace d) => ‖gradW x‖)) (hgradVφ_bdd : BddAbove (Set.range fun (z : PhaseSpace d) => ‖gradVφ z‖)) (t : ℝ) : ∃ (r : ℝ), r = 1 / ↑N ^ 2 * ∑ i : Fin N, inner ℝ (gradW 0) (gradVφ (X t i, V t i)) ∧ HasDerivAt (fun (s : ℝ) => ∫ (z : PhaseSpace d), φ z ∂empiricalMeasureCurve N X V s) (∫ (z : PhaseSpace d), inner ℝ z.2 (gradXφ z) - inner ℝ (convolveFunctionMeasure gradW (spatialMarginal (empiricalMeasureCurve N X V t)) z.1) (gradVφ z) ∂empiricalMeasureCurve N X V t + r) t ∧ |r| ≤ 1 / ↑N * ⨆ (x : PhysSpace d), ‖gradW x‖ * ⨆ (z : PhaseSpace d), ‖gradVφ z‖

(tex: prop:weak) Weak evolution of the empirical measure.

Let (X, V) : [0, T] → (ℝ^d × ℝ^d)^N solve the Newton equations eq:newton, and let ρ_t^N be the spatial marginal of the empirical measure μ_t^N. Then for every test function φ ∈ C_c^∞(ℝ^d × ℝ^d) and every time t, there is a real remainder r = R_N(t) such that

d/dt ⟨μ_t^N, φ⟩ = ⟨μ_t^N, v · ∇_x φ − (∇W * ρ_t^N) · ∇_v φ⟩ + r,

with |r| ≤ (1/N) ‖∇W‖_∞ ‖∇v φ‖∞. Concretely, r is the diagonal correction +(1/N²) Σᵢ ∇W(0) · ∇v φ(xᵢ, vᵢ). (The positive sign arises because extending the Newton-equation sum Σ{j≠i} to Σ_j subtracts the j=i term gradW(0), which then gets multiplied by the outer −(1/N) acceleration coefficient, yielding +(1/N²)·gradW(0)·gradVφ.) Under Assumption ass:W (W even ⟹ ∇W(0) = 0) the diagonal vanishes and r = 0; that strengthening is the content of empiricalMeasureSolvesVlasov below.

The remainder is quantified existentially because HasDerivAt has a unique derivative — a free R_N parameter would make the statement false.

§6 Equation (Weak form of empirical-measure evolution) (tex: eq:weak-eq)

def Vlasov.WeakEvolutionEq {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (μ : ℝ → MeasureTheory.Measure (PhaseSpace d)) (φ : PhaseSpace d → ℝ) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (R_N : ℝ → ℝ) : Prop

(tex: eq:weak-eq) The distributional evolution identity for the empirical measure (the content of Proposition prop:weak):

d/dt ⟨μ_t^N, φ⟩ = ⟨μ_t^N, v · ∇_x φ − (∇W * ρ_t^N) · ∇_v φ⟩ + R_N(t),

for every φ ∈ C_c^∞(ℝ^d × ℝ^d), with |R_N(t)| ≤ (1/N) ‖∇W‖_∞ ‖∇v φ‖∞.

This is a Prop-valued definition packaging the statement of eq:weak-eq.

Equations

• One or more equations did not get rendered due to their size.

§7 Corollary (Empirical measure solves Vlasov) (tex: cor:empirical-vlasov)

theorem Vlasov.empiricalMeasureSolvesVlasov {d : ℕ} (N : ℕ) (W : PhysSpace d → ℝ) [hW : AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (X V : ℝ → Fin N → PhysSpace d) (hSol : IsNewtonSolution N gradW X V) (φ : PhaseSpace d → ℝ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (_hφ_compact : HasCompactSupport φ) (gradXφ gradVφ : PhaseSpace d → PhysSpace d) (hgradXφ : ∀ (z : PhaseSpace d), gradXφ z = gradient (fun (x : PhysSpace d) => φ (x, z.2)) z.1) (hgradVφ : ∀ (z : PhaseSpace d), gradVφ z = gradient (fun (v : PhysSpace d) => φ (z.1, v)) z.2) : WeakEvolutionEq gradW (empiricalMeasureCurve N X V) φ gradXφ gradVφ fun (x : ℝ) => 0

(tex: cor:empirical-vlasov) Under Assumption ass:W, the empirical measure μ_t^N satisfies the distributional Vlasov equation eq:vlasov with remainder R_N ≡ 0: for every φ ∈ C_c^∞(ℝ^d × ℝ^d),

d/dt ⟨μ_t^N, φ⟩ = ⟨μ_t^N, v · ∇_x φ − (∇W * ρ_t^N) · ∇_v φ⟩.

§8 Equation (Vlasov equation) (tex: eq:vlasov)

def Vlasov.IsVlasovSolution {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) : Prop

(tex: eq:vlasov) The nonlinear Vlasov equation for a curve of probability measures f_t on ℝ^d × ℝ^d:

∂_t f + v · ∇_x f − (∇W * ρ_t)(x) · ∇_v f = 0, ρ_t(x) = ∫ f_t(x, dv).

We encode this as the distributional statement: for every φ ∈ C_c^∞(ℝ^d × ℝ^d) the map t ↦ ∫ φ df_t satisfies

d/dt ∫ φ df_t = ∫ [v · ∇_x φ − (∇W * ρ_t)(x) · ∇_v φ] df_t.

Equations

• One or more equations did not get rendered due to their size.

theorem Vlasov.empiricalMeasure_isVlasovSolution {d : ℕ} (N : ℕ) (W : PhysSpace d → ℝ) [AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (X V : ℝ → Fin N → PhysSpace d) (hSol : IsNewtonSolution N gradW X V) : IsVlasovSolution gradW (empiricalMeasureCurve N X V)

(tex: cor:empirical-vlasov, packaged) The empirical measure curve of a global Newton solution is a global (two-sided) weak Vlasov solution — empiricalMeasureSolvesVlasov quantified over the full C_c^∞ test class of IsVlasovSolution, with no hypotheses beyond ass:W. Together with empiricalMeasureCurve_hasFiniteFirstMoment this discharges the weak-PDE and moment sides of the solution predicates on empirical curves; the remaining gap to the IsLagrangianVlasovSolution that dobrushin consumes is the characteristic-flow witness (the linear flow of the empirical field, with atoms following characteristics), which is not yet formalized.

§9 Theorem (Existence and uniqueness for Vlasov) (tex: thm:vlasov-wp)

def Vlasov.HasFiniteFirstMoment {d : ℕ} (μ : MeasureTheory.Measure (PhaseSpace d)) : Prop

Predicate: μ is a probability measure on PhaseSpace d with finite first moment.

Equations

• Vlasov.HasFiniteFirstMoment μ = (MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.Integrable (fun (z : Vlasov.PhaseSpace d) => ‖z‖) μ)

theorem Vlasov.empiricalMeasure_hasFiniteFirstMoment {d : ℕ} (N : ℕ) [NeZero N] (X V : Fin N → PhysSpace d) : HasFiniteFirstMoment (empiricalMeasure N X V)

Empirical measures lie in 𝒫₁: probability (for N ≥ 1) plus finite first moment — the latter because integration against a finite weighted sum of Dirac masses is a finite sum. Discharges, pointwise in time, the moment hypotheses that the Dobrushin-type estimates place on empirical curves.

theorem Vlasov.empiricalMeasureCurve_hasFiniteFirstMoment {d : ℕ} (N : ℕ) [NeZero N] (X V : ℝ → Fin N → PhysSpace d) (t : ℝ) : HasFiniteFirstMoment (empiricalMeasureCurve N X V t)

Curve version of empiricalMeasure_hasFiniteFirstMoment: the empirical measure of a particle configuration lies in 𝒫₁ at every time.

§10 Equation (Characteristic / mean-field ODE) (tex: eq:char)

def Vlasov.IsCharacteristicFlow {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) : Prop

(tex: eq:char) Predicate asserting that (charX, charV) : ℝ → PhaseSpace d → PhysSpace d × PhysSpace d is the characteristic flow associated to a given curve of spatial marginal measures ρ : ℝ → Measure (PhysSpace d) and pair-potential gradient gradW:

X'(t, z) = V(t, z), V'(t, z) = −(∇W * ρ_t)(X(t, z)), (X, V)(0, z) = z.

The self-consistent condition (ρ_t is the pushforward of f_0 under X(t, ·)) is captured by IsCharacteristicFlowSelfConsistent.

Equations

• One or more equations did not get rendered due to their size.

def Vlasov.IsCharacteristicFlowSelfConsistent {d : ℕ} (charX : ℝ → PhaseSpace d → PhysSpace d) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) : Prop

(tex: eq:char) The self-consistency condition: the spatial marginal ρ_t equals the pushforward of the initial spatial marginal f₀_x under the position map X(t, ·).

Equations

• Vlasov.IsCharacteristicFlowSelfConsistent charX f₀ ρ = ∀ (t : ℝ), ρ t = MeasureTheory.Measure.map (fun (z : Vlasov.PhaseSpace d) => charX t z) f₀

noncomputable def Vlasov.vlasovSolutionViaPushforward {d : ℕ} (charX charV : ℝ → PhaseSpace d → PhysSpace d) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (t : ℝ) : MeasureTheory.Measure (PhaseSpace d)

(tex: eq:char) The Vlasov solution f_t is the pushforward of f_0 under the characteristic map (X(t,·), V(t,·)).

Equations

• Vlasov.vlasovSolutionViaPushforward charX charV f₀ t = MeasureTheory.Measure.map (fun (z : Vlasov.PhaseSpace d) => (charX t z, charV t z)) f₀

def Vlasov.IsLagrangianVlasovSolution {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) : Prop

A Vlasov solution with an explicit characteristic-flow representation.

Strictly stronger than IsVlasovSolution: every IsLagrangianVlasovSolution satisfies the weak PDE AND admits a global characteristic flow (charX, charV) such that f t = (charX t, charV t)_# (f 0) for every t.

This is the regularity level at which the dynamic-continuity / Lipschitz-on- flow / dominated-convergence-on-trajectory arguments (upper semicontinuity of W₁ under narrow convergence, the derivative bound feeding Gronwall, narrow continuity in the KR-dual formulation) compose cleanly — these all need the flow witness, which the abstract IsVlasovSolution does not carry.

Producers:

• vlasovSolutionViaPushforward_isLagrangianVlasovSolution (LeanPool/Vlasov/OT/CharacteristicFlow.lean) — takes the flow as a hypothesis, and the pushforward equation holds by vlasovSolutionViaPushforward's definition.
• vlasovWellPosedness produces the per-window family IsLagrangianVlasovSolutionOn gradW f T for every horizon T > 0 (not this global predicate — the flow witnesses may differ per window) from a Banach fixed-point construction on spatial marginals; the characteristic flow falls out of the existence proof, so the windowed Lagrangian conclusion costs no extra infrastructure.

IsLagrangianVlasovSolution gradW f → IsVlasovSolution gradW f by .1.

Equations

• One or more equations did not get rendered due to their size.

§11 Theorem (Dobrushin, 1979) (tex: thm:dobrushin)

theorem Vlasov.exists_wasserstein1_limit_of_cauchy {d : ℕ} (ν : ℕ → MeasureTheory.Measure (PhysSpace d)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (ν n)] (M : ℝ) (hMom : ∀ (n : ℕ), ∫ (y : PhysSpace d), ‖y‖ ∂ν n ≤ M) (h_yint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (ν n)) (hCauchy : ∀ (ε : ENNReal), 0 < ε → ∃ (N : ℕ), ∀ (m n : ℕ), N ≤ m → N ≤ n → wasserstein1 (ν m) (ν n) < ε) : ∃ (μ : MeasureTheory.Measure (PhysSpace d)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) μ ∧ ∫ (y : PhysSpace d), ‖y‖ ∂μ ≤ M ∧ Filter.Tendsto (fun (n : ℕ) => wasserstein1 (ν n) μ) Filter.atTop (nhds 0)

Completeness of (𝒫_1(PhysSpace d), W₁) for Polish spaces.

A Cauchy sequence in W₁ with a uniform first-moment bound has a W₁-limit in 𝒫_1. The proof routes through Prokhorov + tightness from the moment bound

• narrow-to-W₁ upgrade under moment control.

Used to lift the Picard iteration's Cauchy sequence (from the Phi_supW1_contraction contraction estimate) to a W₁-limit in the curve space; the limit is a fixed point of the Picard iteration, yielding a self-consistent characteristic flow + Vlasov solution on [0, T₀].

Note on finiteness in the convolution Lipschitz cascade

convolveLipschitz_KR_le, convolveLipschitz_inner_bound, and norm_convolveFunctionMeasure_sub_le conclude in .toReal of an ENNReal expression involving wasserstein1 ρ σ. The inequality requires a finiteness hypothesis wasserstein1 ρ σ ≠ ⊤: without it (⊤ : ℝ≥0∞).toReal = 0 would collapse any positive LHS bound. The hypothesis is threaded through the cascade and discharged at the Dobrushin call site from HasFiniteFirstMoment via wasserstein1_lt_top_of_finite_moment. See formalize/DESIGN.md (in the source repository).

theorem Vlasov.convolveLipschitz_inner_lipschitz {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (x v : PhysSpace d) : LipschitzWith (L * ‖v‖₊) fun (y : PhysSpace d) => inner ℝ (gradW (x - y)) v

For fixed x : PhysSpace d and v : PhysSpace d, the function y ↦ @inner ℝ (PhysSpace d) _ (gradW (x - y)) v is LipschitzWith (L * ‖v‖₊). Proof: the map y ↦ gradW (x - y) is L-Lipschitz (composition of the L-Lipschitz gradW with the 1-Lipschitz subtraction y ↦ x - y), and w ↦ ⟨w, v⟩ is ‖v‖₊-Lipschitz (bounded linear map with operator norm ‖v‖); compose via LipschitzWith.comp.

theorem Vlasov.convolveLipschitz_KR_le {α : Type u_1} [MeasurableSpace α] [PseudoMetricSpace α] (ρ σ : MeasureTheory.Measure α) (φ : α → ℝ) (hφ : LipschitzWith 1 φ) (hW : wasserstein1 ρ σ ≠ ⊤) : ∫ (y : α), φ y ∂ρ - ∫ (y : α), φ y ∂σ ≤ (wasserstein1 ρ σ).toReal

For any 1-Lipschitz function φ : PhysSpace d → ℝ, the integral difference ∫ φ dρ − ∫ φ dσ ≤ (wasserstein1 ρ σ).toReal. This follows directly from the Kantorovich–Rubinstein definition of wasserstein1 as the supremum of integral differences over 1-Lipschitz test functions, together with ENNReal.toReal_iSup and ENNReal.ofReal_toReal to convert between ENNReal and ℝ.

theorem Vlasov.convolveLipschitz_inner_bound {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ σ : MeasureTheory.Measure (PhysSpace d)) [MeasureTheory.IsProbabilityMeasure ρ] [MeasureTheory.IsProbabilityMeasure σ] (x : PhysSpace d) (hW : wasserstein1 ρ σ ≠ ⊤) (hρ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) ρ) (hσ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) σ) (v : PhysSpace d) : ‖v‖ ≤ 1 → inner ℝ (convolveFunctionMeasure gradW ρ x - convolveFunctionMeasure gradW σ x) v ≤ ↑L * (wasserstein1 ρ σ).toReal

For any v : PhysSpace d with ‖v‖ ≤ 1, the real inner product ⟨(∇W∗ρ)(x) − (∇W∗σ)(x), v⟩ is bounded by (L : ℝ) * (wasserstein1 ρ σ).toReal. Proof: unfold convolveFunctionMeasure to expose ∫ gradW(x−y) dρ and ∫ gradW(x−y) dσ; commute the inner product ⟨·, v⟩ (a continuous linear map) through each integral via ContinuousLinearMap.integral_comp_comm; then the integrand function y ↦ ⟨gradW(x−y), v⟩ has Lipschitz constant L * ‖v‖ ≤ L (from convolveLipschitz_inner_lipschitz), so (1/L) * (that integrand) is 1-Lipschitz and convolveLipschitz_KR_le closes the estimate.

theorem Vlasov.convolveLipschitz_norm_le_of_inner_forall {d : ℕ} (z : PhysSpace d) (C : ℝ) (h : ∀ (v : PhysSpace d), ‖v‖ ≤ 1 → inner ℝ z v ≤ C) : ‖z‖ ≤ C

For z : PhysSpace d and C : ℝ, if every unit vector v (with ‖v‖ ≤ 1) satisfies @inner ℝ (PhysSpace d) _ z v ≤ C, then ‖z‖ ≤ C. Proof: in the z = 0 case, ‖0‖ = 0 ≤ C (from C ≥ ⟨0, 0⟩ = 0); in the z ≠ 0 case, take v = z / ‖z‖ (which satisfies ‖v‖ = 1); then ‖z‖ = ⟨z, z/‖z‖⟩ = ⟨z, v⟩ ≤ C by hypothesis via real_inner_self_eq_norm_mul_norm.

theorem Vlasov.norm_convolveFunctionMeasure_sub_le {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ σ : MeasureTheory.Measure (PhysSpace d)) [MeasureTheory.IsProbabilityMeasure ρ] [MeasureTheory.IsProbabilityMeasure σ] (x : PhysSpace d) (hW : wasserstein1 ρ σ ≠ ⊤) (hρ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) ρ) (hσ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) σ) : ‖convolveFunctionMeasure gradW ρ x - convolveFunctionMeasure gradW σ x‖ ≤ ↑L * (wasserstein1 ρ σ).toReal

theorem Vlasov.continuousOn_integral_of_isLagrangianVlasovSolution {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (hf_lag : IsLagrangianVlasovSolution gradW f) (hf_prob_0 : HasFiniteFirstMoment (f 0)) (T : ℝ) (hT : 0 ≤ T) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (h_y_int : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (spatialMarginal (f t))) (h_conv_int : ∀ (t : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (spatialMarginal (f t))) [∀ (t : ℝ), MeasureTheory.IsProbabilityMeasure (spatialMarginal (f t))] (φ : PhaseSpace d → ℝ) (hφ_lip : LipschitzWith 1 φ) : ContinuousOn (fun (t : ℝ) => ∫ (z : PhaseSpace d), φ z ∂f t) (Set.Icc 0 T)

W₁-continuity of the integral against a Lagrangian Vlasov solution.

Uses the enriched IsLagrangianVlasovSolution predicate (carrying the characteristic flow), which makes the proof structurally clean: by the pushforward equation f t = Measure.map (charX t, charV t) (f 0) and integral_map, ∫ φ d(f t) = ∫ (φ ∘ (charX t, charV t)) d(f 0). Continuity in t then reduces to dominated convergence on the fixed measure f 0, with pointwise continuity from the flow's HasDerivAt and an integrable dominator from HasFiniteFirstMoment (f 0) + a flow-growth bound.

theorem Vlasov.w1_lscNarrow_of_summands {d : ℕ} (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (h_summands : ∀ (φ : PhaseSpace d → ℝ), LipschitzWith 1 φ → LowerSemicontinuousOn (fun (t : ℝ) => ENNReal.ofReal (∫ (z : PhaseSpace d), φ z ∂f t - ∫ (z : PhaseSpace d), φ z ∂g t)) (Set.Icc 0 T)) : LowerSemicontinuousOn (fun (t : ℝ) => wasserstein1 (f t) (g t)) (Set.Icc 0 T)

Given per-1-Lipschitz LSC of each summand t ↦ ENNReal.ofReal(∫φd(f t) - ∫φd(g t)), the Wasserstein-1 distance wasserstein1 (f t) (g t) = ⨆ φ (_ : LipschitzWith 1 φ), … is LowerSemicontinuousOn Set.Icc 0 T as a double supremum of LSC functions via lowerSemicontinuousOn_iSup applied twice.

theorem Vlasov.wassersteinGronwallCoupling_gronwall_le (h : ℝ → ℝ) (δ C T : ℝ) (_hT : 0 ≤ T) (hcont : ContinuousOn h (Set.Icc 0 T)) (hinit : h 0 ≤ δ) (hderiv : ∀ s ∈ Set.Ico 0 T, ∀ (r : ℝ), C * h s < r → ∃ᶠ (z : ℝ) in nhdsWithin s (Set.Ioi s), (z - s)⁻¹ * (h z - h s) < r) (t : ℝ) : t ∈ Set.Icc 0 T → h t ≤ δ * Real.exp (C * t)

For a continuous function h : ℝ → ℝ on [0, T] with h(0) ≤ δ and with right-derivative liminf bounded by C * h(s) for all s ∈ [0, T), Gronwall's inequality gives h(t) ≤ δ * Real.exp(C * t) for all t ∈ [0, T]. This wraps Mathlib's le_gronwallBound_of_liminf_deriv_right_le with ε = 0 and then simplifies via gronwallBound_ε0.

theorem Vlasov.gronwall_mild_le (Q : ℝ → ℝ) (q0 K T : ℝ) (hK : 0 ≤ K) (hq0 : 0 ≤ q0) (hQcont : Continuous Q) (hQnn : ∀ (t : ℝ), 0 ≤ Q t) (hmild : ∀ t ∈ Set.Icc 0 T, Q t ≤ q0 + K * ∫ (s : ℝ) in 0..t, Q s) (t : ℝ) : t ∈ Set.Icc 0 T → Q t ≤ q0 * Real.exp (K * t)

Scalar mild-form Gronwall: a continuous nonnegative Q satisfying the integral inequality Q t ≤ q0 + K · ∫₀ᵗ Q on [0, T] obeys Q t ≤ q0 · exp (K t).

This is the mild-form companion to wassersteinGronwallCoupling_gronwall_le (which takes the Dini/right-derivative form). The integrated coupling-Gronwall bound produces Q(t) = ∫‖Φ_f t · − Φ_g t ·‖ dπ₀ in the integral form (via per-trajectory FTC + Tonelli on a nonnegative integrand), sidestepping the reverse-Fatou difference-quotient interchange. Proof: apply Mathlib's norm_le_gronwallBound_of_norm_deriv_right_le to the C¹ primitive G t = q0 + K · ∫₀ᵗ Q (with G' t = K · Q t ≤ K · G t since Q ≤ G), then Q ≤ G.

theorem Vlasov.wassersteinGronwallCoupling_ennreal_mul_comm (δ : ℝ) (hδ : 0 ≤ δ) (C t : ℝ) : ENNReal.ofReal (δ * Real.exp (C * t)) = ENNReal.ofReal (Real.exp (C * t)) * ENNReal.ofReal δ

For reals δ ≥ 0 and C > 0 and t ≥ 0, if r ≤ δ * Real.exp(C * t) then ENNReal.ofReal r ≤ ENNReal.ofReal (Real.exp (C * t)) * ENNReal.ofReal δ. Uses ENNReal.ofReal_mul and mul_comm to reorder the product.

theorem Vlasov.convolveDiff_norm_le {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ σ : MeasureTheory.Measure (PhysSpace d)) [MeasureTheory.IsProbabilityMeasure ρ] [MeasureTheory.IsProbabilityMeasure σ] (x : PhysSpace d) (hW : wasserstein1 ρ σ ≠ ⊤) (hρ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) ρ) (hσ_int : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) σ) : ‖convolveFunctionMeasure gradW ρ x - convolveFunctionMeasure gradW σ x‖ ≤ ↑L * (wasserstein1 ρ σ).toReal

If gradW is L-Lipschitz, then for any x : PhysSpace d and any two measures ρ, σ on PhysSpace d, ‖(∇Wρ)(x) − (∇Wσ)(x)‖ ≤ L · W₁(ρ,σ).toReal. This is the key estimate: the convolution ∇W * ρ is Lipschitz in ρ with respect to the Wasserstein-1 distance, via Kantorovich–Rubinstein duality. A thin wrapper around norm_convolveFunctionMeasure_sub_le.

def Vlasov.DobrushinStabilityEstimate {d : ℕ} (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (C : ℝ) : Prop

(tex: eq:dobrushin) The exponential Wasserstein-1 stability estimate for Vlasov solutions (the content of Theorem thm:dobrushin):

W_1(f_t, g_t) ≤ e^{C·t} · W_1(f_0, g_0), for all t ≥ 0.

This Prop-valued definition packages the statement as a reusable predicate.

Equations

• Vlasov.DobrushinStabilityEstimate f g C = ∀ (t : ℝ), 0 ≤ t → Vlasov.wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (C * t)) * Vlasov.wasserstein1 (f 0) (g 0)

§13 Corollary (Mean-field limit) (tex: cor:mfl)

theorem Vlasov.meanFieldLimit {d : ℕ} (W : PhysSpace d → ℝ) (gradW : PhysSpace d → PhysSpace d) (_hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (_hL : LipschitzWith L gradW) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (_hf₀ : HasFiniteFirstMoment f₀) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (_hf_sol : IsLagrangianVlasovSolution gradW f) (hf_init : f 0 = f₀) (X V : (N : ℕ) → ℝ → Fin N → PhysSpace d) (_hSol : ∀ (N : ℕ), IsNewtonSolution N gradW (X N) (V N)) (hInit : Filter.Tendsto (fun (N : ℕ) => wasserstein1 (empiricalMeasure N (X N 0) (V N 0)) f₀) Filter.atTop (nhds 0)) (C : ℝ) (hC : 0 < C) (hDobrushin : ∀ (N : ℕ), DobrushinStabilityEstimate (empiricalMeasureCurve N (X N) (V N)) f C) (T : ℝ) (_hT : 0 < T) : Filter.Tendsto (fun (N : ℕ) => ⨆ t ∈ Set.Icc 0 T, wasserstein1 (empiricalMeasureCurve N (X N) (V N) t) (f t)) Filter.atTop (nhds 0)

(tex: cor:mfl) Mean-field limit theorem.

Let f_0 ∈ 𝒫_1(ℝ^d × ℝ^d) and let (X^N, V^N) be the N-particle Newton trajectories. Write μ_0^N for the initial empirical measure of (X^N(0), V^N(0)). If μ_0^N → f_0 in W_1 as N → ∞ then, under Assumption ass:W and the Dobrushin estimate, for every T > 0,

sup_{t ∈ [0,T]} W_1(μ_t^N, f_t) ≤ e^{C·T} · W_1(μ_0^N, f_0) → 0, as N → ∞.

f_t is the unique Vlasov solution with initial datum f_0 (Theorem thm:vlasov-wp). The .tex names the initial data (X_0^N, V_0^N); here we identify them with X N 0 and V N 0 rather than introducing redundant X₀, V₀ parameters that would need a separate hypothesis to link them to the trajectory.