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_localand its Picard / final-assembly sub-helpers); - the fixed-
T_0continuation tower — the one-window glue stepvlasovWellPosedness_glue(with itsvlasovGlue_*helper family),exists_localSmallness_window, and the forward iteration to arbitraryT_target; - per-window uniqueness over
IsLagrangianVlasovSolutionOnand the universal-in-tbridge toIsLagrangianVlasovSolution; - 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 constantC = 2 · max 1 L, whose hypotheses are exactly the clausesvlasovWellPosednessemits.
See formalize/DESIGN.md (in the source repository) for the overall design.
§9 Theorem (Existence and uniqueness for Vlasov) (tex: thm:vlasov-wp) #
Lipschitz growth of the force plus a first moment of the measure make the
shifted force integrable. The workhorse integrability fact behind every
convolveFunctionMeasure estimate.
LocalSmallnessContraction L T IS the Grönwall contraction factor
gronwallBound 0 (max 1 L) L T < 1, after unfolding both definitions.
Sub-helper for vlasovWellPosedness_local — the Picard fixed-point
self-consistent flow.
Given f₀ : Measure (PhaseSpace d) with finite first moment, produces a
characteristic flow (charX, charV) whose own pushforward's spatial
marginal is the reference measure the flow is built against — i.e., the
Picard fixed point at the spatial-marginal-curve level:
ρ_t := spatialMarginal (Measure.map (z ↦ (charX t z, charV t z)) f₀)
charX, charV solve the Vlasov ODE against this ρ.
The body carries the substantive Picard analysis:
- M-fixed-point: pick a moment bound
M ≥ A/(1 - B)whereA = gronwallBound 1 (1+L) ‖gradW 0‖ T · (M_f₀ + 1)andB = L · (exp((1+L)·T) - 1)/(1+L) · (M_f₀ + 1). RequiresB < 1, which is the genuine convergence criterion for the moment iteration (stronger than the contraction predicateLocalSmallnessContraction L Talone for largeM_f₀— the contraction predicate gates the q factor; the M-fixed-point additionally requires the moment iteration to converge). - Picard sequence
x_n : ℕ → VlasovMeasureCurve d T Mstarting fromx_0 := constantCurve (spatialMarginal f₀)andx_{n+1} := Phi_step(x_n). - Contraction via
Phi_supW1_contraction:supW1On (Φρ) (Φσ) ≤ q · Dwithq < 1. Applypicard_iterate_isCauchy_of_contraction+picard_iterate_exists_limitto get the W₁-limitρ_lim : VlasovMeasureCurve d T M. - Self-consistency
Φ(ρ_lim) = ρ_lim: triangle throughx_n. - Apply
exists_vlasov_characteristicFlow_global_smallTtoρ_lim.extendto get the flow.
Metric-dependence note. The convergence rests on two independent predicates:
LocalSmallnessContraction L T := L · (exp((max 1 L)·T) - 1) / (max 1 L) < 1— exponential in T, fromPhi_supW1_contraction's W₁-based shape.LocalSmallnessPLBuffer L T := L · T² < 1— quadratic, from per-ball Picard-Lindelöf's ball geometry.
These are genuinely independent (neither universally implies the other), so each predicate matches its own sub-argument.
Under the Wbar refactor (Dobrushin 1979, §5), both constraints become
linear-in-T and align: LocalSmallnessContraction reduces to
C₂(L)·T < 1, and the single algebraic constraint then suffices and is
satisfiable for any L > 0 by taking T < 1/C₂(L).
Output bundle (designed to feed
vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn directly):
- Flow
(charX, charV)against the spatial marginal of the pushforward — the load-bearing self-consistency conjunct. - Boundary regularity.
- Uniform moment bound
M_ρon the spatial marginal trajectory.
Sub-helper for vlasovWellPosedness_local — moment-bound transport.
Given the Picard fixed-point flow's bundle (from
_picard_fixedPointFlow), produces HasFiniteFirstMoment (f t) for
t ∈ Icc 0 T, where f := vlasovSolutionViaPushforward charX charV f₀.
Proof strategy:
- Boundary transport: extract
h_init / h_cont_Icc / h_deriv_Icofromhflow_on + h_boundaryviacharacteristicFlow_boundary_regularity. flow_distance_growth_bound_onapplied to(charX, charV)produces the growth constantC_Twith‖(charX t z, charV t z)‖ ≤ C_T * (‖z‖ + 1).- Probability of
f t = Measure.map (z ↦ (charX t z, charV t z)) f₀from the AEMeasurable witness. - Integrable
‖·‖onf t: viaintegrable_map_measure+ growth bound +Integrable ‖·‖ f₀.
Factored out to keep vlasovWellPosedness_local's body a clean glue.
Sub-helper for vlasovWellPosedness_local — IsLagrangianVlasovSolutionOn
threading.
Given the Picard fixed-point flow's bundle (from
_picard_fixedPointFlow), produces the
IsLagrangianVlasovSolutionOn gradW f T conjunct via the 20-hypothesis
threading through
vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn.
Proof strategy:
- Boundary transport: extract
h_init / h_cont_Icc / h_deriv_Ico. - Universal-in-
sconvolution integrability (handlingsoutside[0, T]via the clamp-extension argument). - AEMeasurable witness.
IsCharacteristicFlowSelfConsistent:∀ t, ρ_lim t = Φ charX f₀ t, which expands by definition sinceρ_lim = spatialMarginal ∘ fandf = vlasovSolutionViaPushforward charX charV f₀; spatial marginal of pushforward = pushforward underProd.fst ∘ ...=Φ charX f₀. The composition is theMeasure.map_map-with-AEMeasurable bridge.- Continuity of
gradW:hL.continuous. - Probability instance of
spatialMarginal ∘ f: derived from AEMeasurable + IsProbabilityMeasure f₀. - Final invocation:
vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOnwith the full hypothesis bundle.
Factored out to keep vlasovWellPosedness_local's body a clean glue.
Local existence of a Vlasov solution on [0, T].
Under the joint constraint LocalSmallnessPLBuffer L T (L · T² < 1) +
LocalSmallnessContraction L T, produces a local-time Vlasov solution
f : ℝ → Measure (PhaseSpace d) on [0, T] satisfying initial
condition + local finite first moment + IsLagrangianVlasovSolutionOn.
The forward-iteration continuation extends from local T to arbitrary
T_target via fixed-T_0 iteration: the contraction time T_0
depends only on L (not on the moment bound M_n propagating through
iterations), because Phi_supW1_contraction's q is
gronwallBound 0 (max 1 L) (L · D) T — independent of M_n. So the
continuation iterates [0, T_0], [T_0, 2 T_0], … with constant step T_0,
reaching any T_target in ⌈T_target / T_0⌉ windows; gluing then bridges
from IsLagrangianVlasovSolutionOn (local) to IsLagrangianVlasovSolution
(global).
Proof strategy:
Initial spatial marginal:
μ₀ := spatialMarginal f₀. ByHasFiniteFirstMoment f₀,μ₀is a probability measure withIntegrable ‖·‖. LetM_f₀ := ∫ ‖z‖ ∂f₀(finite byhf₀.2.integral_norm_le).Picard sequence on spatial marginals:
ρ_0 := constantCurve μ₀.ρ_{n+1}obtained viaPhi_stepapplied toρ_n's flow.
Each
ρ_nlives inVlasovMeasureCurve d T Mfor an appropriateMchosen so that the growth bound fromflow_distance_growth_bound_onstays withinMacross iterations (the M-preservation constraint).Contraction estimate via
Phi_supW1_contraction:supW1On (ρ_n.ρ) (ρ_{n+1}.ρ) ≤ ENNReal.ofReal (q^n * D₀)forq := gronwallBound 0 (max 1 L) (L · D) T < 1(sinceTis small enough per the joint constraint).Apply
picard_iterate_isCauchy_of_contractionto get the ENNReal-form Cauchy condition on thesupW1Onpseudodistance.Apply
picard_iterate_exists_limitto extract the limitρ_lim : VlasovMeasureCurve d T Mplus pointwise W₁-tendsto.Self-consistency
Φ(ρ_lim) = ρ_lim: triangle throughρ_nusing the uniform-tendsto helper, contraction, and pointwise tendsto.Apply
exists_vlasov_characteristicFlow_global_smallTtoρ_lim.extendto get the characteristic flow(charX, charV)against the self-consistent limit.Define
f := vlasovSolutionViaPushforward charX charV f₀. Verify:f 0 = f₀(fromIsCharacteristicFlowOn's initial-condition clause +Measure.map_id).HasFiniteFirstMoment (f t)on[0, T](fromflow_distance_growth_bound_onapplied to(charX, charV)+hf₀.2).IsLagrangianVlasovSolutionOn gradW f TviavlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn.
The body invokes vlasovWellPosedness_local_picard_fixedPointFlow for the
Picard fixed-point flow, then vlasovWellPosedness_local_finalAssembly_*
for the moment and Lagrangian conjuncts, deriving f 0 = f₀ inline.
Banked infrastructure: localized hasDerivAt_of_hasDerivAt_of_ne #
Local version of hasDerivAt_of_hasDerivAt_of_ne (Mathlib/Analysis/Calculus/
FDeriv/Extend.lean): if f : ℝ → ℝ has HasDerivAt with derivative g(y) at
every y ≠ x₀ in some neighborhood of x₀, and both f and g are continuous
at x₀, then f has HasDerivAt with derivative g(x₀) at x₀.
The proof composes hasDerivWithinAt_Iic_of_tendsto_deriv (left side) +
hasDerivWithinAt_Ici_of_tendsto_deriv (right side) + HasDerivWithinAt.union,
following the Mathlib lemma's proof structure but with locally-quantified
hypothesis (enabling use when the punctured-HasDerivAt holds only on a bounded
interval, not all of ℝ).
Variable-T_target continuation via fixed-T_0 iteration #
Route 2 inner kernel for glue_step h_cont_g (LEFT / Iic T): continuity
at the seam T of s ↦ (∇W ∗ μ_s)(charX s z), where the window measure curve μ is
the flow-pushforward of f₀.
Proven from PROVEN tools only (no deferred OT). The pushforward rewrite
(∇W ∗ μ_s)(x) = ∫ z', gradW (x − charX s z') ∂f₀ (integral_map) turns the
moving-measure convolution into a fixed-f₀ integral with moving integrand, closed by
dominated convergence: convergence from the flow's seam continuity h_charX_cont,
domination from the Gronwall growth bound hC_T (Piece A) against f₀'s finite first
moment. This is the structural reason h_cont_g does NOT need the general narrow→W₁
kernel — its consumer carries a pushforward representation.
Route 2 inner kernel for glue_step h_cont_g (RIGHT / Ici a): the
exact mirror of flowConv_continuousWithinAt_Iic_seam, but on Set.Ici a over a
generic window [a, b] with the seam at the lower endpoint a. Same proof shape;
the only set-dependent swaps are Iic T → Ici a, Icc_mem_nhdsLE → Icc_mem_nhdsGE,
and the window [0, T] → [a, b]. Used for the RIGHT side of the seam at T where
charX is the composed position flow Z_s z = charX_g (s-T) (charX_prev T z, …) and
μ s = spatialMarginal (g (s-T)) is its pushforward of f₀.
One-window glue step.
Given a solution f_prev : ℝ → Measure (PhaseSpace d) on [0, T]
satisfying the local-existence conjuncts (initial condition + finite first
moment + IsLagrangianVlasovSolutionOn), and a window length T_0
satisfying the smallness constraints LocalSmallnessPLBuffer L T_0 +
LocalSmallnessContraction L T_0, produces a glued solution
f_next : ℝ → Measure (PhaseSpace d) on [0, T + T_0] that agrees with
f_prev on [0, T].
Proof strategy:
Shift the initial condition: apply
vlasovWellPosedness_localtof_prev T(which has finite first moment byh_prev_mom T) with window lengthT_0. Gives a solutiong : ℝ → Measure (PhaseSpace d)on[0, T_0]withg 0 = f_prev T.Glue: define
f_next t := if t ≤ T then f_prev t else g (t - T). Agreement att = Tis byg 0 = f_prev T.Verify the four output conjuncts:
- Initial:
f_next 0 = f_prev 0 = f₀. - Moment: piecewise from
h_prev_momandg's moment bound. IsLagrangianVlasovSolutionOnon[0, T + T_0]:IsVlasovSolutionOn: weak PDE onIoo 0 (T + T_0)— split atT, useh_prev_lag.1forIoo 0 Tpart andg's forIoo T (T+T_0), continuity atTfrom the integral being continuous.- Flow: glue the per-window flows via standard ODE composition (charX_next(t, z) := if t ≤ T then charX_prev(t, z) else charX_g(t - T, (charX_prev(T, z), charV_prev(T, z)))).
- Pushforward equation: holds piecewise.
- AEMeasurable witness: composition of AEMeasurable maps.
- Initial:
For every positive Lipschitz constant there is a window length satisfying all
three per-window smallness constraints — the PL buffer, the contraction, and the
envelope closure. Pure threshold arithmetic: T_0 := min(1/√L, T_0_con, T_0_env)/2
with each threshold positive for every L > 0 (no L < 1 restriction).
Forward iteration to arbitrary T_target.
Extends the local-existence theorem from its small-T smallness window
to any T_target > 0, by iterating the local theorem with shifted initial
data at a fixed step T_0 depending only on L (no L < 1 hypothesis).
Proof strategy:
Pick
T_0 := min(T_0_PL, T_0_con, T_0_env) / 2, withT_0_PL := 1/√L(the PL-buffer threshold forL · T_0² < 1),T_0_con/T_0_envthe contraction/envelope thresholds. Each is positive for everyL > 0, soT_0 > 0and all three smallness constraints hold.Pick
N := ⌈T_target / T_0⌉₊so thatN · T_0 ≥ T_target.Nat.recconstruction: a solution holding the conjuncts atT = n·T_0.- Base case: apply
vlasovWellPosedness_localdirectly. - Step case (
n → n+1): applyvlasovWellPosedness_glueto extend.
- Base case: apply
Take
f := f_Nand verify the conjuncts forT_target ≤ N · T_0viaIsLagrangianVlasovSolutionOn's monotonicity inT(project down).
Uniqueness over IsLagrangianVlasovSolutionOn per window #
Uniqueness on the local window.
Two IsLagrangianVlasovSolutionOns with the same initial data agree on
[0, T_target].
Proof (closed via Dobrushin uniqueness composition):
- Extract
IsVlasovSolutionOnfrom eachIsLagrangianVlasovSolutionOn. - Note
f 0 = f₀ = g 0from the init hypotheses. - Apply
dobrushin_uniqueness_On(localized Dobrushin uniqueness, the private helper above) to concludef t = g t.
Universal-in-t bridge to IsLagrangianVlasovSolution #
IsLagrangianVlasovSolutionOn is antitone in the window length: a Lagrangian
solution on [0, T] restricts to one on any [0, T'] ⊆ [0, 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.
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:
Apply
vlasovWellPosedness_forwardwithT_target := nfor eachn : ℕ, getting per-nsolutionsf_n : ℝ → Measure (PhaseSpace d).By
vlasovWellPosedness_uniqueness,f_nandf_magree onIcc 0 (min n m).Define
f t := f_{⌈t⌉ + 1} tfort ≥ 0. By step 2, this is well-defined ont ≥ 0.IsLagrangianVlasovSolutionOn gradW f T_targetfor eachT_target: composes from the per-window solutions.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) #
(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 #
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.
(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.
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.
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.
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).
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)
Instances For
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).