Well-posedness ladder for the Vlasov equation + Dobrushin stability

This file builds on the characteristic-flow infrastructure of LeanPool/Vlasov/OT/CharacteristicFlow.lean and carries the theorem ladder of the development:

• §9 local existence and uniqueness (vlasovWellPosedness_local and its Picard / final-assembly sub-helpers);
• the fixed-T_0 continuation tower — the one-window glue step vlasovWellPosedness_glue (with its vlasovGlue_* helper family), exists_localSmallness_window, and the forward iteration to arbitrary T_target;
• per-window uniqueness over IsLagrangianVlasovSolutionOn and the universal-in-t bridge to IsLagrangianVlasovSolution;
• the §10 marquee results: vlasovWellPosedness (forward-in-time existence), vlasovWellPosedness_uniqueness, dobrushin (W₁ stability, proved by coupling the two flows and a Grönwall estimate), and the mean-field limit;
• the wiring layer dobrushin_on / dobrushin_forward / vlasovWellPosedness_stability: the window and forward-global stability forms with the explicit uniform constant C = 2 · max 1 L, whose hypotheses are exactly the clauses vlasovWellPosedness emits.

See formalize/DESIGN.md (in the source repository) for the overall design.

Uniqueness over IsLagrangianVlasovSolutionOn per window

theorem Vlasov.vlasovWellPosedness_uniqueness {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₀) {T_target : ℝ} (hT_target : 0 < T_target) (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (hf_init : f 0 = f₀) (hg_init : g 0 = f₀) (hf_mom : ∀ t ∈ Set.Icc 0 T_target, HasFiniteFirstMoment (f t)) (hg_mom : ∀ t ∈ Set.Icc 0 T_target, HasFiniteFirstMoment (g t)) (hf_lag : IsLagrangianVlasovSolutionOn gradW f T_target) (hg_lag : IsLagrangianVlasovSolutionOn gradW g T_target) (t : ℝ) : t ∈ Set.Icc 0 T_target → f t = g t

Uniqueness on the local window.

Two IsLagrangianVlasovSolutionOns with the same initial data agree on [0, T_target].

Proof (closed via Dobrushin uniqueness composition):

1. Extract IsVlasovSolutionOn from each IsLagrangianVlasovSolutionOn.
2. Note f 0 = f₀ = g 0 from the init hypotheses.
3. Apply dobrushin_uniqueness_On (localized Dobrushin uniqueness, the private helper above) to conclude f t = g t.

Universal-in-t bridge to IsLagrangianVlasovSolution

theorem Vlasov.IsLagrangianVlasovSolutionOn.mono_window {d : ℕ} {gradW : PhysSpace d → PhysSpace d} {g : ℝ → MeasureTheory.Measure (PhaseSpace d)} {T T' : ℝ} (h : IsLagrangianVlasovSolutionOn gradW g T) (hTT' : T' ≤ T) : IsLagrangianVlasovSolutionOn gradW g T'

IsLagrangianVlasovSolutionOn is antitone in the window length: a Lagrangian solution on [0, T] restricts to one on any [0, T'] ⊆ [0, T].

theorem Vlasov.integral_continuousWithinAt_of_flow_rep {d : ℕ} (f₀ : MeasureTheory.Measure (PhaseSpace d)) [MeasureTheory.IsProbabilityMeasure f₀] (fcur : ℝ → MeasureTheory.Measure (PhaseSpace d)) (Φ : ℝ → PhaseSpace d → PhaseSpace d) (g : PhaseSpace d → ℝ) (hg_cont : Continuous g) (C : ℝ) (hgC : ∀ (z : PhaseSpace d), ‖g z‖ ≤ C) (B t₀ : ℝ) (ht₀B : t₀ ∈ Set.Icc 0 B) (h_integral_eq : ∀ t ∈ Set.Icc 0 B, ∫ (z : PhaseSpace d), g z ∂fcur t = ∫ (z : PhaseSpace d), g (Φ t z) ∂f₀) (h_aesm : ∀ t ∈ Set.Icc 0 B, MeasureTheory.AEStronglyMeasurable (fun (z : PhaseSpace d) => g (Φ t z)) f₀) (h_ptcont : ∀ (z : PhaseSpace d), ContinuousWithinAt (fun (t : ℝ) => Φ t z) (Set.Icc 0 B) t₀) : ContinuousWithinAt (fun (t : ℝ) => ∫ (z : PhaseSpace d), g z ∂fcur t) (Set.Icc 0 B) t₀

Continuity (within a window, at a point) of t ↦ ∫ g d(fcur t) for a curve represented on the window as a flow pushforward: dominated convergence against the fixed f₀, then transfer along the representation.

theorem Vlasov.vlasovWellPosedness_universal_existence {d : ℕ} [NeZero d] (W : PhysSpace d → ℝ) (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (hL_pos : 0 < ↑L) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (hf₀ : HasFiniteFirstMoment f₀) : ∃ (f : ℝ → MeasureTheory.Measure (PhaseSpace d)), f 0 = f₀ ∧ (∀ t ∈ Set.Ici 0, HasFiniteFirstMoment (f t)) ∧ (∀ (T_target : ℝ), 0 < T_target → IsLagrangianVlasovSolutionOn gradW f T_target) ∧ ∀ (g : PhaseSpace d → ℝ), Continuous g → Bornology.IsBounded (Set.range g) → ContinuousOn (fun (t : ℝ) => ∫ (z : PhaseSpace d), g z ∂f t) (Set.Ici 0)

Universal-in-t (forward) existence — bridge to the marquee form.

For any Lipschitz constant L > 0, produces a single f : ℝ → Measure (PhaseSpace d) satisfying IsLagrangianVlasovSolutionOn for every T_target > 0, with finite first moment and narrow continuity on Ici 0. Composes vlasovWellPosedness_forward (forward iteration) + vlasovWellPosedness_uniqueness (agreement on overlaps).

Proof strategy:

1. Apply vlasovWellPosedness_forward with T_target := n for each n : ℕ, getting per-n solutions f_n : ℝ → Measure (PhaseSpace d).

2. By vlasovWellPosedness_uniqueness, f_n and f_m agree on Icc 0 (min n m).

3. Define f t := f_{⌈t⌉ + 1} t for t ≥ 0. By step 2, this is well-defined on t ≥ 0.

4. IsLagrangianVlasovSolutionOn gradW f T_target for each T_target: composes from the per-window solutions.

5. Narrow continuity on Ici 0: standard DCT using moment bound + flow growth.

The problem is a forward Cauchy problem; backward time is not on the critical path.

§10 Marquee theorem (tex: thm:vlasov-wp)

theorem Vlasov.vlasovWellPosedness {d : ℕ} [NeZero d] (W : PhysSpace d → ℝ) [AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL_gradW : LipschitzWith L gradW) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (hf₀ : HasFiniteFirstMoment f₀) : ∃ (f : ℝ → MeasureTheory.Measure (PhaseSpace d)), f 0 = f₀ ∧ (∀ t ∈ Set.Ici 0, HasFiniteFirstMoment (f t)) ∧ (∀ (T_target : ℝ), 0 < T_target → IsLagrangianVlasovSolutionOn gradW f T_target) ∧ ∀ (g : PhaseSpace d → ℝ), Continuous g → Bornology.IsBounded (Set.range g) → ContinuousOn (fun (t : ℝ) => ∫ (z : PhaseSpace d), g z ∂f t) (Set.Ici 0)

(tex: thm:vlasov-wp) Forward-in-time existence for the Vlasov equation.

Let f_0 ∈ 𝒫_1(ℝ^d × ℝ^d) be a probability measure with finite first moment. Under Assumption ass:W, for an arbitrary Lipschitz constant of gradW, there exists a narrowly continuous curve t ↦ f_t ∈ 𝒫_1(ℝ^d × ℝ^d) on [0, ∞), with f_{t=0} = f_0, solving eq:vlasov in the Lagrangian sense on every forward window [0, T_target].

Per-window uniqueness over the Lagrangian class is provided separately by vlasovWellPosedness_uniqueness. The proof case-splits on L = 0 (constant force, explicit solution) vs 0 < L (the substantive forward-iteration path), and holds for every L (no smallness restriction).

§10 Dobrushin stability chain

theorem Vlasov.dobrushin_package_exists {d : ℕ} (W : PhysSpace d → ℝ) [_hW : AssW W] (gradW : PhysSpace d → PhysSpace d) (_hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (hf : IsLagrangianVlasovSolution gradW f) (hg : IsLagrangianVlasovSolution gradW g) (hf_prob : ∀ (t : ℝ), HasFiniteFirstMoment (f t)) (hg_prob : ∀ (t : ℝ), HasFiniteFirstMoment (g t)) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (C * t)) * wasserstein1Coupling (f 0) (g 0)

Package the bound and positivity of C into the existential conclusion of dobrushin: ∃ C > 0, ∀ t ≥ 0, W₁(f_t, g_t) ≤ exp(C·t) · W₁(f_0, g_0). Depends on dobrushin_C_choice (in Basic.lean) and dobrushin_ennreal_bound.

theorem Vlasov.dobrushin {d : ℕ} (W : PhysSpace d → ℝ) [hW : AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (hf : IsLagrangianVlasovSolution gradW f) (hg : IsLagrangianVlasovSolution gradW g) (hf_prob : ∀ (t : ℝ), HasFiniteFirstMoment (f t)) (hg_prob : ∀ (t : ℝ), HasFiniteFirstMoment (g t)) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (C * t)) * wasserstein1 (f 0) (g 0)

(tex: thm:dobrushin) Dobrushin's stability theorem (1979).

Under Assumption ass:W, there exists a constant C = C(L) > 0 such that for any two measure-valued solutions f_t, g_t ∈ 𝒫_1(ℝ^d × ℝ^d) of the Vlasov equation eq:vlasov,

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

where W_1 is the Wasserstein-1 distance. The proof uses a coupling via the characteristic flows eq:char and a Gronwall inequality; the key estimate is |∇W * ρ − ∇W * σ|_∞ ≤ L · W_1(ρ, σ).

The [AssW W] instance and hgradW record the standing setup ass:W (∇W the gradient of an even C^{1,1} potential); the inequality itself consumes only the Lipschitz bound hL — see dobrushin_on below for the minimal-hypothesis window form with the explicit constant C = 2 · max 1 L.

theorem Vlasov.dobrushin_on {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf : IsLagrangianVlasovSolutionOn gradW f T) (hg : IsLagrangianVlasovSolutionOn gradW g T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hg_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (g t)) (t : ℝ) : t ∈ Set.Icc 0 T → wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (2 * ↑(max 1 L) * t)) * wasserstein1 (f 0) (g 0)

Dobrushin stability on the window [0, T] — the public form of the uniform-constant estimate, with the dual W₁ metric on both sides.

Unlike the marquee dobrushin (global two-sided solutions, existential constant), this form (i) consumes exactly what vlasovWellPosedness emits — per-window IsLagrangianVlasovSolutionOn plus window moments — and (ii) exposes the explicit constant C = 2 · max 1 L, which depends only on the force's Lipschitz bound, not on the solution pair. That uniformity is what a mean-field argument quantifying over a family of solutions (e.g. empirical curves, once their flow witnesses are formalized) needs.

theorem Vlasov.dobrushin_forward {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (f g : ℝ → MeasureTheory.Measure (PhaseSpace d)) (hf : ∀ (T : ℝ), 0 < T → IsLagrangianVlasovSolutionOn gradW f T) (hg : ∀ (T : ℝ), 0 < T → IsLagrangianVlasovSolutionOn gradW g T) (hf_mom : ∀ t ∈ Set.Ici 0, HasFiniteFirstMoment (f t)) (hg_mom : ∀ t ∈ Set.Ici 0, HasFiniteFirstMoment (g t)) (t : ℝ) : 0 ≤ t → wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (2 * ↑(max 1 L) * t)) * wasserstein1 (f 0) (g 0)

Forward-global Dobrushin stability with the explicit uniform constant.

Stability for the solution class vlasovWellPosedness constructs: the hypotheses are verbatim the existence theorem's conclusion clauses (the per-window IsLagrangianVlasovSolutionOn family on every horizon, moments on Set.Ici 0), and the estimate holds for all t ≥ 0 with the pair-independent constant C = 2 · max 1 L. This is the arrow that lets the existence output feed a Dobrushin-type stability input; see vlasovWellPosedness_stability for the packaged composition.

theorem Vlasov.vlasovWellPosedness_stability {d : ℕ} [NeZero d] (W : PhysSpace d → ℝ) [AssW W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f₀ g₀ : MeasureTheory.Measure (PhaseSpace d)) (hf₀ : HasFiniteFirstMoment f₀) (hg₀ : HasFiniteFirstMoment g₀) : ∃ (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (g : ℝ → MeasureTheory.Measure (PhaseSpace d)), f 0 = f₀ ∧ g 0 = g₀ ∧ (∀ (T : ℝ), 0 < T → IsLagrangianVlasovSolutionOn gradW f T) ∧ (∀ (T : ℝ), 0 < T → IsLagrangianVlasovSolutionOn gradW g T) ∧ ∀ (t : ℝ), 0 ≤ t → wasserstein1 (f t) (g t) ≤ ENNReal.ofReal (Real.exp (2 * ↑(max 1 L) * t)) * wasserstein1 f₀ g₀

Well-posedness package: existence + stability, chained.

For any two initial data f₀, g₀ ∈ 𝒫₁, the curves produced by vlasovWellPosedness satisfy the Dobrushin estimate with the explicit constant C = 2 · max 1 L at every t ≥ 0 — the composition of the two headline theorems, recorded so that the existence output demonstrably feeds the stability input (dobrushin_forward).

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

Coupling-metric Dobrushin stability estimate — the wasserstein1Coupling (primal) analogue of DobrushinStabilityEstimate (Basic). LHS is the genuine dual W₁ metric; the RHS base is the primal coupling-inf metric wasserstein1Coupling. This is the form the B-free core (dobrushin_package_exists) produces.

Equations

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

theorem Vlasov.meanFieldLimit_coupling {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 : ℕ) => wasserstein1Coupling (empiricalMeasure N (X N 0) (V N 0)) f₀) Filter.atTop (nhds 0)) (C : ℝ) (hC : 0 < C) (hDobrushin : ∀ (N : ℕ), DobrushinStabilityEstimateCoupling (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)

Mean-field limit — B-free coupling form.

The meanFieldLimit (Basic) analogue that consumes the coupling-metric stability estimate (DobrushinStabilityEstimateCoupling, produced B-free by dobrushin_package_exists) and coupling-metric initial convergence (wasserstein1Coupling (μ_0^N) f₀ → 0). The conclusion is unchanged: convergence of the empirical curves to the Vlasov solution in the genuine dual W₁ metric. Axiom-clean (#print axioms): B-free.

Why coupling-hInit — the initial-convergence type the B-free limit requires. The B-free estimate puts wasserstein1Coupling on the RHS base, so the squeeze needs wasserstein1Coupling (μ_0^N) f₀ → 0. Standard dual-W₁ initial convergence does NOT supply this B-free: wasserstein1 ≤ wasserstein1Coupling (wasserstein1_le_wasserstein1Coupling), so dual-small does not bound the coupling — the easy direction runs the wrong way for a hypothesis; converting dual→coupling is the hard direction (= Foundation B, wasserstein1_eq_coupling). The two are mathematically equal (KR duality) and coupling-convergence is the natural form for empirical measures (one exhibits couplings to bound the cost from above), so this is a nominal — not a real — strengthening. The all-dual meanFieldLimit (Basic) remains the standard-hypothesis form, routing through the all-dual dobrushin (the single Foundation-B bridge).