Characteristic flow for the Vlasov ODE + Lagrangian-Eulerian equivalence #
This file builds on LeanPool/Vlasov/OT/Coupling.lean and provides the flow-side
infrastructure of the development:
- existence of the characteristic flow for the Vlasov field
(
exists_vlasov_characteristicFlow), via the vendored Picard–Lindelöf wrapper and a tight per-window construction valid for arbitrary Lipschitz constant; - the Lagrangian → Eulerian equivalence — the pushforward of
f₀under the characteristic flow satisfies the weak Vlasov equation; - the localized solution predicates and the pushforward operator
Φfeeding the well-posedness ladder, which lives inLeanPool/Vlasov/OT/WellPosedness.leantogether with the marquee results.
The Grönwall step rests on the force estimate
‖∇W∗ρ − ∇W∗σ‖ ≤ L·W₁(ρ, σ) (norm_convolveFunctionMeasure_sub_le) and on
wasserstein1_pushforward_le_iInf from Coupling.lean.
Mathlib-upstream targeting note. The position-Lipschitz of
convolution against a probability measure and the Picard-Lindelöf
wrapper for a phase-space ODE are domain-independent and Mathlib-
worthy; they would naturally live alongside the OT chapter in
Mathlib/MeasureTheory/Wasserstein/CharacteristicFlow.lean or split
between Mathlib/Analysis/ODE/ and the OT chapter. The Lagrangian →
Eulerian equivalence (pushforward of f₀ under the characteristic
flow satisfies the weak Vlasov equation) is the genuine project
responsibility — a Fubini + measure-map +
differentiation-under-integral check that is not in Mathlib.
See formalize/DESIGN.md (in the source repository) for the overall design.
Vlasov velocity field and its Lipschitz lemma #
The Vlasov phase-space vector field:
b_t(x, v) := (v, −(∇W ∗ ρ_t)(x)).
Note that the first component is the identity in v (the position
ODE x' = v) and the second component is the mean-field force
−∇W ∗ ρ_t evaluated at x (the velocity ODE v' = −(∇W ∗ ρ)(x)).
Equations
- Vlasov.vlasovVectorField gradW ρ t z = (z.2, -Vlasov.convolveFunctionMeasure gradW (ρ t) z.1)
Instances For
Position-side Lipschitz of the convolution ∇W ∗ ρ.
For gradW L-Lipschitz and ρ a probability measure with finite
first moment (which guarantees integrability of the kernel), the map
x ↦ (∇W ∗ ρ)(x) is L-Lipschitz.
Proof sketch: by LipschitzWith.dist_le_mul applied pointwise to
gradW, then integration over the probability measure ρ:
‖∫ y, gradW(x−y) ∂ρ − ∫ y, gradW(x'−y) ∂ρ‖
= ‖∫ y, (gradW(x−y) − gradW(x'−y)) ∂ρ‖
≤ ∫ y, ‖gradW(x−y) − gradW(x'−y)‖ ∂ρ
≤ ∫ y, L · ‖x − x'‖ ∂ρ
= L · ‖x − x'‖ · ρ(univ)
= L · ‖x − x'‖ (probability measure).
The integrability hypotheses on gradW(x − ·) for two distinct xs
are needed for integral_sub and norm_integral_le_integral_norm
to fire. At the dobrushin call site these follow from finite first
moment of ρ + Lipschitz growth of gradW.
Flow distance growth bound (Gronwall on the characteristic ODE) #
A standalone regularity theorem about IsCharacteristicFlow: solutions of
the characteristic ODE have at most linear growth in their initial condition,
with a constant depending on T, the Lipschitz constant of gradW, and a
uniform first-moment bound on the measure curve ρ.
Math content: Gronwall on the position-velocity pair, using
‖(∇W ∗ ρ_t)(x)‖ ≤ ‖gradW 0‖ + L · (‖x‖ + ∫‖y‖dρ_t)
as the velocity-field bound.
Flow distance growth bound (L-Lipschitz gradW, uniform first moment
on ρ). Solutions of the characteristic ODE grow at most linearly in their
initial condition: ‖(charX t z, charV t z)‖ ≤ C_T · (‖z‖ + 1) for some
C_T depending only on T, L, ‖gradW 0‖, and the uniform first-moment
bound M_ρ.
Two-flow difference Gronwall bound — the reusable core of the
integrated Dobrushin coupling bound. The distance between two trajectories
Φ_f · z₁, Φ_g · z₂ of flows generated by fields b_f, b_g (b_f
L-Lipschitz in space) grows by Gronwall: if the field difference at the
second trajectory is bounded by ε on [0, T] and the initial separation by
δ, then ‖Φ_f t z₁ - Φ_g t z₂‖ ≤ gronwallBound δ L ε t.
Mirrors flow_distance_growth_bound's Gronwall structure
(norm_le_gronwallBound_of_norm_deriv_right_le) but for the difference of two
flows. In the integrated-bound application, z₁ = ω.1, z₂ = ω.2 range over a
coupling π₀ of (f 0, g 0), ε = (L : ℝ) * (wasserstein1 (f s) (g s)).toReal
(the self-coupling diff-bound, uniform in the trajectory), and integrating this
pointwise bound over π₀ against the pushforward bound gives the Dobrushin
estimate W₁(f t, g t) ≤ … · W₁(f 0, g 0).
Per-trajectory mild (integral-form) difference bound.
Mild-form companion to flow_difference_growth_bound:
the raw integral inequality
‖γ_f t − γ_g t‖ ≤ ‖γ_f 0 − γ_g 0‖ + ∫₀ᵗ (L‖γ_f s − γ_g s‖ + ε s) ds,
keeping the forcing ε s inside the integral. After integrating this over
the base measure, the self-reference ε s = L·W₁(f s,g s) ≤ L·Q(s) is resolved
by gronwall_mild_le — avoiding the constant-ε smallness that
flow_difference_growth_bound's closed form would force (and the blocked
windowing that smallness needs).
Integrate a per-trajectory mild bound over the base measure (Tonelli step).
Given a base probability measure π on Ω and a family w : ℝ → Ω → α, if each
trajectory satisfies the mild bound ‖w t ω‖ ≤ ‖w 0 ω‖ + ∫₀ᵗ (L‖w s ω‖ + ε s) ds,
then the integrated quantity Q t := ∫ ‖w t ω‖ ∂π satisfies
Q t ≤ Q 0 + ∫₀ᵗ (L · Q s + ε s) ds. The ∫₀ᵗ L‖w s ω‖ term swaps via Tonelli.
Integrated coupling-Gronwall bound (base-measure generic).
Given a base probability measure π on Ω and two parameter-families of
trajectories X_f, X_g : ℝ → Ω → α solving ODEs with L-Lipschitz vector fields
b_f, b_g on [0, T], with a cross-field bound ‖b_f s y - b_g s y‖ ≤ ε s whose
amplitude ε s is self-referentially controlled by the integrated trajectory
distance Q s := ∫ ω, ‖X_f s ω - X_g s ω‖ ∂π (i.e. ε s ≤ L · Q s), the
integrated distance obeys the closed Gronwall bound
Q t ≤ Q 0 · exp (2 L t) on [0, T].
Composition (the collapse pipeline):
- per-
ω,flow_difference_mild_boundgives the mild integral inequality‖X_f t ω - X_g t ω‖ ≤ ‖X_f 0 ω - X_g 0 ω‖ + ∫₀ᵗ (L‖X_f s ω - X_g s ω‖ + ε s); integral_mild_boundintegrates this overπ(Tonelli on a nonnegative integrand), yieldingQ t ≤ Q 0 + ∫₀ᵗ (L·Q s + ε s);- the self-reference
ε s ≤ L·Q scollapses the integrand to2 L · Q s; gronwall_mild_le(scalar mild Gronwall) closes toQ 0 · exp (2 L t).
Clamp bridge: integral_mild_bound and the DCT continuity of Q
require global-in-s continuity, but the flow regularity is only on the
window [0, T]. We work with the clamped flow s ↦ X_f (clamp s) ω (globally
continuous, agreeing with X_f on [0, T]), apply the window machinery to it,
and transfer back on [0, T] where clamp = id via integrand congruence.
Base-measure genericity: π is abstract, so this serves both the
uniqueness call site (π = f 0, Q 0 = 0, Foundation-B-free) and the
mean-field call site (π an optimal coupling, Q 0 = W₁(f 0, g 0)).
IsCharacteristicFlowOn-flavored variant of flow_distance_growth_bound.
Same Gronwall growth bound, but for a flow specified by boundary regularity
hypotheses (h_init, h_cont_Icc, h_deriv_Ico) instead of the universal-in-t
ODE of IsCharacteristicFlow. This matches what
exists_vlasov_characteristicFlow_global_smallT produces (modulo deriving the
boundary regularity from IsCharacteristicFlowOn's Ioo 0 T ODE clauses), and
mirrors the hypothesis-passing pattern of charFlow_measurable_via_gronwall.
Used by: Phi_step to derive the per-z growth bound
(PhiAsVlasovMeasureCurve's h_growth hypothesis); window uniqueness is a
natural secondary consumer.
Proof body: identical to flow_distance_growth_bound's except the three
hflow-derived facts (h_f_cont, h_deriv, h_init_norm) are now taken
directly from the boundary regularity hypotheses. Same Gronwall step, same
final algebra.
Metric-dependence note:
This bound uses the unbounded position difference ‖X^M(t,z) - X^{M'}(t,z)‖,
which forces Gronwall and produces exponential-in-T constants
C_T ≈ exp((1+L)·T). The Wbar = W_{min(|x-y|,1)} analog (Dobrushin 1979, §5)
uses the bounded-and-Lipschitz absorption
|B_μ(x) - B_{μ'}(x)| ≤ max(2‖B‖_∞, C_B) · min(|x₁-x₂|, 1)
and produces linear-in-T constants (Dobrushin 1979, eq. 5.7), changing this
output shape from C_T · (‖z‖ + 1) to a bounded analog.
Piece A (Option 2): time-dependent moment-envelope growth bound.
Sharper sibling of flow_distance_growth_bound_on. Instead of a single
constant moment bound M_ρ (which forces the constant-sup growth constant
C_T and, downstream, an M_f₀-dependent fixed-point on the curve space),
this takes a monotone time-dependent envelope m : ℝ → ℝ bounding the
spatial-marginal first moment, and concludes the time-local Gronwall bound
‖(charX t z, charV t z)‖ ≤ gronwallBound ‖z‖ (1+L) (‖gradW 0‖ + L · m t) t,
with the force constant ε(t) = ‖gradW 0‖ + L · m t evaluated at the SAME time
t (not the sup m T). Monotonicity of m lets the per-t Gronwall on
[0, t] use the endpoint value ε(t) while validating the derivative bound at
every s ≤ t (since ε(s) ≤ ε(t)).
Why this is the option-2 foundation: integrating the conclusion over a
probability f₀ gives M_{Φρ}(t) ≤ A(t) + B(t)·m(t) with
A(t) = M_f₀·e^{(1+L)t} + (‖gradW 0‖/(1+L))(e^{(1+L)t}-1) and
B(t) = (L/(1+L))(e^{(1+L)t}-1) — crucially an M_f₀-free coefficient.
The canonical envelope m*(t) := A(t)/(1-B(T)) is then Φ-invariant under the
data-independent constraint B(T) < 1, dissolving the constant-M
fixed-point without a data-dependent hypothesis. (Contrast the constant-sup
bound, which feeds m(T) into ε and re-derives an M_f₀-dependent
smallness.)
Piece A.3 (Option 2): the canonical moment envelope closes (data-free).
Pure-algebra companion to flow_distance_growth_bound_on_timedep. Under the
M_f₀-free smallness B(T) := (L/(1+L))(e^{(1+L)T}-1) < 1, the explicit
envelope m*(t) := gronwallBound M_f₀ (1+L) g0 t / (1 - B(T)) is a Gronwall
super-solution:
- monotone on
[0, T], - dominates the initial moment
M_f₀, - Φ-invariant at the moment level:
gronwallBound M_f₀ (1+L) (g0 + L·m* t) t ≤ m* t.
Composed with Piece A integrated over f₀ (which gives
M_{Φρ}(t) ≤ gronwallBound M_f₀ (1+L) (g0 + L·m(t)) t, g0 = ‖gradW 0‖), this
shows the Picard iterates stay inside the fixed envelope m* with no
data-dependent hypothesis — the faithful dissolution of the constant-M
fixed-point. This lemma is the measure-free heart of the option-2 escape;
Pieces B–D thread it through the curve space, Phi_step, and #11.
Piece A.2 (Option 2): integrate the per-z growth bound to a moment bound.
The measure-level bridge between Piece A and Piece A.3: given the per-z
time-local growth bound (Piece A's conclusion, taken here as the hypothesis
h_growth so this lemma is decoupled from the flow construction), the
position pushforward Measure.map (charX t ·) f₀ has first moment bounded
by the same Gronwall functional evaluated at the initial moment ∫‖z‖ ∂f₀:
∫ x, ‖x‖ ∂(Measure.map (charX t ·) f₀) ≤ gronwallBound (∫‖z‖ ∂f₀) (1+L) (g0 + L·m t) t.
Proof: integral_map exchanges the pushforward; ‖charX t z‖ ≤ ‖(charX t z, charV t z)‖
h_growthbounds the integrand bygronwallBound ‖z‖ …, which is affine in‖z‖, so itsf₀-integral isgronwallBound (∫‖z‖) …(probability measure ⇒ the constant term integrates to itself).
Composing with gronwall_envelope_exists (Piece A.3): when m = m* the canonical
envelope and g0 = ‖gradW 0‖, the RHS is ≤ m* t, i.e. Φ maps the envelope to
itself at the moment level — the measure-level statement of the data-free escape.
Characteristic flow existence (Picard-Lindelöf wrapper) #
This section wraps the vendored parametric Picard-Lindelöf theorem
(LeanPool.Vlasov.ForMathlib.PicardLindelof) to extract a characteristic flow
(charX, charV) for the Vlasov ODE.
The four IsPicardLindelof hypotheses (Lipschitz-on-ball,
continuous-in-time, norm bound, contraction) are derived from
convolveFunctionMeasure_lipschitz_in_x, plus narrow-continuity of the
spatial-marginal curve ρ, plus a uniform norm bound from the
finite-mass assumption.
The contraction condition L · max(tmax − t₀, t₀ − tmin) ≤ a − r
pins down the local time-interval size relative to the ball radius.
For the dobrushin application we work on a finite interval [0, T];
the existence theorem is parametrised by T and produces a flow
on Set.Icc 0 T (extending the local flow by stitching overlapping
windows; technically a separate iteration argument, deferred to
the proof body).
This sub-section first establishes the global Lipschitz constant
for vlasovVectorField (a direct composition of
convolveFunctionMeasure_lipschitz_in_x with the 1-Lipschitz
identity on the velocity coordinate, combined via LipschitzWith.prodMk).
The global Lipschitz immediately restricts to any closed ball,
giving the first of the four IsPicardLindelof fields.
The full exists_vlasov_characteristicFlow proof packages the global
norm bound into a per-window IsPicardLindelof, invokes the vendored
Picard-Lindelöf (exists_vlasov_extend_one_window), and stitches
N = ⌈T/δ⌉ windows per-z via HasDerivWithinAt.union under the
position/velocity inductive invariant. Downstream callers discharge its
hR/hbound hypotheses; the single-ball hR discharge in
exists_vlasov_trajectory is what introduces the
LocalSmallnessPLBuffer L T := L·T² < 1 constraint — see that
theorem's docstring for the arbitrary-L discussion.
Localized variant of IsCharacteristicFlow from Basic.lean:
the same initial condition + position/velocity ODEs, but quantified
over a chosen time set s_t : Set ℝ and initial-condition set
s_z : Set (PhaseSpace d).
The global IsCharacteristicFlow gradW ρ charX charV is the
specialisation IsCharacteristicFlowOn ... Set.univ Set.univ
(modulo the unconditional init clause).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Monotonicity of IsCharacteristicFlowOn in both the time set and the
initial-condition set. Used at the end of the global existence theorem
to restrict a flow produced on Ioo 0 (N·δ) (covering all of [0, T])
down to Ioo 0 T.
Localized Vlasov-solution predicates on [0, T] #
The globally-quantified predicates IsVlasovSolution and
IsLagrangianVlasovSolution (both in Basic.lean) require the weak PDE and
the characteristic flow to hold universally in t : ℝ. For local existence
(vlasovWellPosedness_local), the Picard iteration only produces a solution
on a small time window [0, T₀]; the underlying characteristic flow comes
from exists_vlasov_characteristicFlow_global_smallT, which exposes
IsCharacteristicFlowOn ... (Ioo 0 T) Set.univ — open-interval ODE
behaviour, not the universal-in-t form IsCharacteristicFlow demands.
The _On-localized predicates below mirror the global ones with their
quantification restricted to [0, T]. Local existence produces the
localized predicate; the forward-iteration continuation glues local windows
to recover the universal-in-t IsLagrangianVlasovSolution required by the
marquee vlasovWellPosedness theorem.
The _On family lives in this file so it can compose with
IsCharacteristicFlowOn (which lives here too); the global versions stay in
Basic.lean as the abstract endpoints.
Localized weak Vlasov evolution equation on Ioo 0 T. Same as
WeakEvolutionEq (Basic.lean) but with the derivative claim
restricted to the open interval t ∈ Set.Ioo 0 T.
Why Ioo not Icc: the characteristic flow only provides
ODE behaviour on Ioo 0 T (the boundary derivatives at t = 0 and
t = T are genuinely unavailable from open-interval HasDerivAt alone).
The Vlasov solution's weak PDE inherits the same regularity: it holds on
the open interval where the characteristic flow is differentiable, and
the initial condition at t = 0 is captured separately by the
pushforward equation in IsLagrangianVlasovSolutionOn.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Localized Vlasov solution on [0, T]. Mirror of IsVlasovSolution
with the weak PDE restricted to [0, T] via WeakEvolutionEqOn.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Localized Lagrangian Vlasov solution on [0, T]. Mirror of
IsLagrangianVlasovSolution (Basic.lean) with:
- the weak PDE restricted to
[0, T](viaIsVlasovSolutionOn), - the characteristic flow restricted to
IsCharacteristicFlowOn ... (Ioo 0 T) Set.univ(the natural output shape of the flow construction), - the initial-condition clause stated explicitly (since
IsCharacteristicFlowOn's initial-condition clause is overs_z, hereSet.univ, so it gives the same content; we restate it for direct usability), - the pushforward equation restricted to
t ∈ Set.Icc 0 T, - the AEMeasurability clause restricted to
s ∈ Set.Icc 0 T.
Every conjunct is the localized analogue of IsLagrangianVlasovSolution's.
The forward-iteration continuation bridges to the global predicate by gluing
local windows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A global IsVlasovSolution restricts to IsVlasovSolutionOn T for any
T : ℝ. Projects the universal HasDerivAt claim onto Ioo 0 T by direct
specialization (the restricted set is open, so HasDerivAt and
HasDerivWithinAt coincide there).
A global IsLagrangianVlasovSolution restricts to
IsLagrangianVlasovSolutionOn T for any T : ℝ.
The flow witness restricts via IsCharacteristicFlowOn's natural relationship
to the universal IsCharacteristicFlow (open Ioo ⊆ ℝ). The pushforward and
AEMeasurability conjuncts restrict trivially since the originals are
universal.
Global Lipschitz constant for the Vlasov phase-space vector field.
b_t(x, v) = (v, -(∇W ∗ ρ_t)(x)) is max(1, L)-Lipschitz when
gradW is L-Lipschitz: the velocity-side projection (x, v) ↦ v
is 1-Lipschitz (LipschitzWith.prod_snd), and the force-side map
(x, v) ↦ -(∇W ∗ ρ_t)(x) is L-Lipschitz (compose
convolveFunctionMeasure_lipschitz_in_x with Neg.neg and
Prod.fst, both 1-Lipschitz). Combining the two via
LipschitzWith.prodMk yields max(1, L) on the product.
Pointwise norm bound for the Vlasov phase-space vector field.
‖b_t(x, v)‖ ≤ max(‖v‖, ‖(∇W ∗ ρ_t)(x)‖) for the product max-norm
on PhaseSpace d = PhysSpace d × PhysSpace d.
This is the decomposition used to derive IsPicardLindelof.norm_le
once a uniform bound M for ‖(∇W ∗ ρ_t)(x)‖ on a closed ball is
known (e.g. from finite-first-moment + Lipschitz growth of gradW).
Local-flow existence for the Vlasov ODE.
Wraps the vendored parametric Picard-Lindelöf
(IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt_confined,
LeanPool.Vlasov.ForMathlib.PicardLindelof)
into a HasDerivAt-on-Ioo-shaped characteristic flow. The result
holds for initial conditions inside closedBall z₀ (a/2) and for
times in Ioo 0 δ where δ is a Picard-derived constant.
The new hypothesis hbound (uniform norm bound on the convolution
force on a slightly larger ball, over [0, 1]) is the genuine input
the Picard wrapper needs: the contraction condition + the norm_le
field of IsPicardLindelof both require a global bound on ‖b_t‖.
The global existence form exists_vlasov_characteristicFlow (below)
is the stitched version on [0, T], iterating this local theorem on
overlapping windows and gluing with ODE_solution_unique.
Per-z, time-shifted single-trajectory Picard with a uniform velocity-bound parameter.
Given a fixed phase-space point w, a starting time t_start, an a priori
velocity bound V_max ≥ ‖w.2‖, and a uniform force bound around w on the
time interval [t_start, t_start + 1], this produces a single trajectory
β : ℝ → PhaseSpace d solving the Vlasov ODE on Ioo t_start (t_start + δ)
with β t_start = w.
Why V_max as a separate parameter: the Picard contraction time δ
depends on the norm-bound L_pl := V_max + a + M for the vector field on
the local ball. Phrasing this via an explicit V_max ≥ ‖w.2‖ rather than
the tight ‖w.2‖ makes δ uniform in w for any iteration centered at
points w whose velocity component is bounded by V_max. This is the
input that lets the N-window iteration in
exists_vlasov_characteristicFlow pick a single δ valid across all
windows (by combining with the a priori bound
‖w_n(z).2‖ ≤ ‖z₀.2‖ + a/2 + M·(T+1) on a finite [0, T]-interval).
Implementation: build an IsPicardLindelof centered at w over [t_start, t_start + δ] with L_pl := V_max + a + M. Invoke the vendored headline
theorem. Take the single trajectory β t := α w t.
Per-window helpers for the N-window induction in #
`exists_vlasov_characteristicFlow`.
These three top-level lemmas are generic in `(β, ODE, confinement,
field bound, IH bound, reference point)` with no mention of the
N-window induction context (no `γ_k`, `k`, `N`, `z₀`). This
genericity gives each helper its own elaboration budget AND makes
them composable for future call sites — the Lagrangian → Eulerian
chain rule, well-posedness's Banach iteration, etc.
Composition order: Helper 1 (confinement) → Helper 2 (window-wide
velocity bound) → Helper 3 (endpoint position bound).
Helper 1: Picard window confinement (projection from phase-space ball).
For a trajectory β satisfying the Vlasov ODE on a Picard window
[t_start, t_start + δ] centered at w, the position component
stays within the local force-bound ball:
(β s).1 ∈ closedBall w.1 (3a/2) for s in the window.
Argument. The strengthened Picard-Lindelöf theorem
exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt_confined
(LeanPool.Vlasov.ForMathlib.PicardLindelof) exposes
FunSpace.compProj_mem_closedBall at the public theorem level,
delivering β s ∈ closedBall w a (phase-space ball of radius a —
the outer Lipschitz radius) as a side product of the existence
guarantee. We project this to the position component via
Prod.dist_eq + le_max_left, then loosen a ≤ 3a/2 by arithmetic.
The result is a 3-5 line projection.
Hypothesis hβ_confined is supplied by Vlasov-side callers from
the widened exists_vlasov_extend_one_window output. The other
hypotheses (ODE, field
bound, contraction inequality) are retained for genericity / call
site compatibility; they are not consumed by the projection body but
remain available for future call sites that want to re-derive the
confinement directly (e.g. via supremum trick) without invoking
the vendored Mathlib API.
Helper 2: Window-wide velocity bound.
For a trajectory β with velocity-component ODE
(β · ).2' = -(∇W ∗ ρ_·)((β ·).1) on [t_start, t_start + δ] and
force bound M (made applicable by h_β_in_ball), the velocity at
every interior s is bounded by h_vel_init + M · (s - t_start).
Math sketch. One application of
Convex.norm_image_sub_le_of_norm_hasDerivWithin_le on (β · ).2
over the convex window Icc t_start (t_start + δ), with y := s
universally quantified:
‖(β s).2 - (β t_start).2‖ ≤ M · ‖s - t_start‖ = M · (s - t_start).
Triangle with ‖(β t_start).2‖ = ‖w.2‖ ≤ h_vel_init (using hβ_init)
gives the conclusion.
The universal quantification over y in the mean-value lemma is what
makes this WINDOW-WIDE from ONE invocation — no per-s re-application.
Helper 3: Window endpoint position bound.
For a trajectory β with position-component ODE
(β · ).1' = (β · ).2 on [t_start, t_start + δ] and a uniform
velocity bound V_bound (typically Helper 2's output composed with
a worst-case substitution), the position at t_start + δ is bounded
relative to an explicit reference point x_ref:
‖(β (t_start + δ)).1 - x_ref‖ ≤ h_pos_init + V_bound · δ
where h_pos_init ≥ ‖w.1 - x_ref‖.
Math sketch. One application of
Convex.norm_image_sub_le_of_norm_hasDerivWithin_le on (β · ).1
over the convex window with x := t_start, y := t_start + δ:
‖(β (t_start + δ)).1 - (β t_start).1‖ ≤ V_bound · δ (using
hβ_init for (β t_start).1 = w.1).
Triangle with ‖w.1 - x_ref‖ ≤ h_pos_init gives the conclusion.
Genericity. x_ref : PhysSpace d is an explicit parameter, NOT
hardcoded to the N-window induction's z₀.1. This makes the helper
reusable for the Lagrangian → Eulerian chain rule (reference point:
support of test function φ), well-posedness's Banach iteration
(reference point: fixed-point candidate), etc.
Tight per-window Picard with an EXPLICIT step δ and an ADAPTIVE force-window.
Tight form of exists_vlasov_extend_one_window: the force bound is required
only on [t_start, t_start + δ] (the actual step), not the loose unit window
[t_start, t_start + 1], and δ is supplied by the caller (so the N-window
chain can tile exactly, N·δ = T, dissolving the (T+1)² → T² smallness).
Tight global per-ball flow: [0,T] force-window, T² smallness (no +1).
Tight form of exists_vlasov_characteristicFlow. By tiling [0,T]
EXACTLY (N = ⌈T/δ_max⌉ windows of width δ' = T/N ≤ δ_max, so N·δ' = T) and
calling exists_vlasov_extend_one_window_tight with the adaptive force-window
[k·δ', (k+1)·δ'], the global force-bound is required only on [0,T] and the
position drift is M·T² (not M·(T+1)²). Consumers' R-selection then needs only
L·T² < 1, satisfiable for any L (threshold T < 1/√L), dissolving the L<1
restriction.
Two-window characteristic-flow existence.
A flow on Ioo 0 (2δ) for some δ > 0 and initial conditions in
closedBall z₀ (a/2). Produces a strictly longer window than
exists_vlasov_characteristicFlow_local (which gave Ioo 0 δ with
the larger δ := (a/2)/(L_pl + 1)); here we tighten the contraction
constraint to L_pl · (2δ) ≤ a/2, yielding the smaller
δ := (a/2)/(2·(L_pl + 1)) but covering a 2δ-long interval.
Implementation note. This is a single Picard call (the vendored
_confined wrapper) with
tmax = 2δ, not a literal "two-window stitch" via uniqueness on
overlapping windows. Mathematically the two are equivalent: a
single Picard with an extended tmax and tightened δ recovers the
same set of solutions that a two-window stitch would produce. The
genuine two-window stitch (per-z second Picard at varying centers
glued via ODE_solution_unique) becomes essential only when the
single-Picard contraction cannot be satisfied — i.e., when the total
time window needed exceeds the asymptotic threshold ≈ 1/2 regardless
of a. For the upcoming N-window induction follow-up, this single-
Picard extension is iterated, with each iteration using a per-z
center from the previous window's endpoint.
Lagrangian → Eulerian: pushforward solves weak Vlasov #
The pushforward vlasovSolutionViaPushforward charX charV f₀ satisfies
IsVlasovSolution. This connects the ODE side (IsCharacteristicFlow,
pointwise HasDerivAt) to the PDE side (IsVlasovSolution,
WeakEvolutionEq distributional formulation), closing the Lagrangian-
Eulerian loop that Mathlib does not provide.
Decomposition. Four named helpers, used as black boxes by the wrapper:
- SC.1
vlasov_pushforward_integral_eq_compose— change of variables:∫ φ d(map flow_s f₀) = ∫ (φ ∘ flow_s) df₀. Directintegral_map. - SC.2
vlasov_traj_chain_rule— pointwise chain rule:HasDerivAt (s ↦ φ (charX s z, charV s z)) [formula] t, usinghflow's ODE pointwiseHasDerivAts and the chain rule onφ. - SC.3
vlasov_pushforward_hasDerivAt_under_integral— differentiation-under-integral viahasDerivAt_integral_of_dominated_loc_of_lip. Requires a dominated-integrable Lipschitz bound ons ↦ φ ∘ flow_suniform inz; this is the diff-under-integral technical heart. - SC.4
vlasov_rhs_pushforward_back— push the chain-rule RHS back throughintegral_mapto matchWeakEvolutionEq's shape. Symmetric to SC.1.
The wrapper composes them: SC.1 (rewrite LHS) → SC.3 (diff-under-integral,
consuming SC.2 pointwise) → SC.4 (rewrite RHS), together with the
AE-strong-measurability of the dot-product integrand (continuity threading
via smoothness of φ and Lipschitz of gradW).
SC.1: integral change-of-variables for the Vlasov pushforward.
Direct application of integral_map.
SC.2: pointwise chain rule along the characteristic trajectory.
For fixed t and fixed z, the curve s ↦ φ (charX s z, charV s z)
has derivative
⟨charV t z, gradXφ (charX t z, charV t z)⟩ − ⟨(∇W ∗ ρ_t)(charX t z), gradVφ (charX t z, charV t z)⟩
at t. Proof: chain rule on φ ∘ (charX · z, charV · z), using
hflow's pointwise HasDerivAts and the gradient formula for φ's
directional derivative.
_at variant of SC.2: pointwise chain rule at a specific (t, z).
Mirror of vlasov_traj_chain_rule (just above), generalized to take the
flow's HasDerivAt hypotheses at the specific (t, z) of interest rather
than universally ∀ t z. This is the form needed by the _On PDE
transport: the flow construction produces IsCharacteristicFlowOn ... (Ioo 0 T) Set.univ which gives HasDerivAt only at t ∈ Ioo 0 T, so
the universal-t form can't be supplied.
This _at variant is the foundation; downstream _on variants of the
SC.5-SC.8 helpers and the vlasov_pushforward_hasDerivAt_under_integral
consumer all compose against this one.
Proof body: identical to vlasov_traj_chain_rule's body modulo the
hypothesis-naming. The original uses hX_deriv t z, hV_deriv t z
exactly once each (at the prodMk step); we replace these with
hX_deriv_at, hV_deriv_at directly. All other steps are
specific-(t, z) already.
Dominated-bundle data for SC.3.
Packages the four ancillary hypotheses required by Mathlib's
hasDerivAt_integral_of_dominated_loc_of_lip (excluding the pointwise
HasDerivAt which SC.2 already provides):
- a neighborhood
nhd ∈ nhds ton which the dominated Lipschitz bound holds; - eventual AE-strong-measurability of
(z ↦ φ ∘ flow_s)forsneart; - integrability of the integrand at
s = t; - AE-strong-measurability of the pointwise derivative as a function of
z; - a
bound : PhaseSpace d → ℝwithIntegrable bound f₀such that, ae-z, the curves ↦ φ(charX s z, charV s z)isReal.nnabs (bound z)-Lipschitz onnhd.
The dominated-bound clause is the technical heart: deriving it requires
a uniform-in-z bound on the flow speed (charV s z, V'(s,z)) on the
support of φ, which the eventual vlasovWellPosedness caller will
produce from Picard-Lindelof local-flow boundedness + HasCompactSupport φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SC.3: differentiation under the integral for the pushforward integral.
HasDerivAt (s ↦ ∫ z, φ (charX s z, charV s z) ∂f₀) (∫ z, [pointwise deriv] ∂f₀) t,
where the pointwise derivative at t is the chain-rule formula from SC.2.
Proven by direct application of Mathlib's
hasDerivAt_integral_of_dominated_loc_of_lip, given the
DiffUnderIntegralData bundle and the pointwise derivative from SC.2.
Taking h_data : DiffUnderIntegralData ... as a hypothesis keeps SC.3's
body a one-line Mathlib application; the burden of producing the
dominated-bundle data moves to the caller (discharged from compact support
of φ plus Picard regularity).
SC.4: push the chain-rule RHS back through integral_map.
∫ z, [formula(charX t z, charV t z)] df₀ = ∫ y, [formula(y)] d(map flow_t f₀).
Symmetric to SC.1; the same integral_map invocation, applied to the
dot-product integrand. Closes by integral_map after establishing AE-
strong-measurability of the integrand.
Lagrangian → Eulerian bundle sub-helpers (SC.5 – SC.8) #
The DiffUnderIntegralData bundle inside the wrapper is decomposed
into four named regularity sub-helpers:
- SC.5
vlasov_compose_flow_aestronglymeas— eventual AE-strong-measurability ofφ ∘ flow_sneart. - SC.6
vlasov_compose_flow_integrable_at— integrability ofφ ∘ flow_tagainstf₀(usesHasCompactSupport φ). - SC.7
vlasov_pointwise_deriv_aestronglymeas— AE-strong- measurability of the chain-rule pointwise derivative (same shape as the wrapper'sh_integrand_aesmproof). - SC.8
vlasov_trajectory_lipschitz_bound— the dominated Lipschitz bound ons ↦ φ(charX s z, charV s z)with anf₀-integrable Lipschitz coefficient, from a uniform velocity bound onnhd × (flow_t)⁻¹(supp φ).
SC.5: AE-strong-measurability of φ ∘ flow_s for s near t.
The composition z ↦ φ (charX s' z, charV s' z) is AE-strongly-
measurable wrt f₀ for every s', in particular for s' in any
neighborhood of t. Uses continuity of φ plus
h_flow_meas's AE-measurability of the flow pair.
SC.6: Integrability of φ ∘ flow_t against f₀.
HasCompactSupport φ + Continuous φ give boundedness; combined with
[IsProbabilityMeasure f₀] this yields integrability.
SC.7: AE-strong-measurability of the pointwise derivative.
The chain-rule pointwise derivative integrand
⟨charV t z, gradXφ(flow_t z)⟩ - ⟨convolve_t(charX t z), gradVφ(flow_t z)⟩
is AE-strongly-measurable wrt f₀. Same continuity argument as the
wrapper's h_integrand_aesm proof.
_lag variant of SC.8 — vlasov_trajectory_lipschitz_bound with the
flow-growth prerequisites supplied as explicit hypotheses, enabling the
dominated Lipschitz bound to be derived via Gronwall on the characteristic
ODE (see flow_distance_growth_bound above). Used by _lag variants
of the Lagrangian → Eulerian chain that route through
IsLagrangianVlasovSolution.
_on variant of SC.8 — vlasov_trajectory_lipschitz_bound with
IsCharacteristicFlowOn ... (Ioo 0 T) Set.univ instead of universal
IsCharacteristicFlow, and with boundary regularity hypotheses
(h_init, h_cont_Icc, h_deriv_Ico) supplied explicitly. Required by
the _On PDE transport (vlasovSolutionViaPushforward_isVlasovSolutionOn).
The body transports vlasov_trajectory_lipschitz_bound_lag's argument with
two substitutions:
flow_distance_growth_bound→flow_distance_growth_bound_on, using the boundary regularity hypotheses.(hflow_x s z).prodMk (hflow_v s z)→hflow_on.2.1 s ... z ...forsin the chosen neighborhood (withinIoo 0 T).
The neighborhood nhd is chosen to stay within Ioo 0 T (where hflow_on
is defined), e.g. Ioo (max 0 (t/2)) (min T (t + 1/2)).
_On-flavored Lagrangian → Eulerian producer for IsVlasovSolutionOn.
The _on analog of vlasovSolutionViaPushforward_isVlasovSolution,
taking the characteristic flow in IsCharacteristicFlowOn ... (Set.Ioo 0 T) Set.univ form (the flow construction's natural output) and
producing the weak Vlasov PDE in localized IsVlasovSolutionOn form (also
on Ioo 0 T).
The global proof's structure transports to the _On form:
intro tbecomesintro t htwithht : t ∈ Set.Ioo 0 T.hflow.2.1 t z(HasDerivAt universal) becomeshflow_on.2.1 t ht z (Set.mem_univ z)(HasDerivAt at the specifict ∈ Ioo 0 T,z ∈ Set.univ).- The conclusion stays at
HasDerivAt(sincet ∈ Ioois an interior point of the predicate's quantification set; noHasDerivWithinAtconversion needed). - The sub-helpers
vlasov_traj_chain_rule,vlasov_compose_flow_*,vlasov_pushforward_hasDerivAt_under_integral,vlasov_rhs_pushforward_backall consume flow hypotheses at a specifict, not universally, so they transport unchanged after threading theht : t ∈ Ioo 0 Tconstraint.
_On-flavored Lagrangian → Eulerian producer for IsLagrangianVlasovSolutionOn.
Same hypothesis package as the global
vlasovSolutionViaPushforward_isLagrangianVlasovSolution, but takes the
characteristic flow in IsCharacteristicFlowOn ... (Set.Ioo 0 T) Set.univ
form (the flow construction's natural output) and produces the strictly
stronger IsLagrangianVlasovSolutionOn predicate.
Composes:
vlasovSolutionViaPushforward_isVlasovSolutionOn(above) for the weak-PDE conjunct.- the flow construction's output for the flow-witness conjunct.
- Trivial pushforward + AEMeasurability bundling for the remaining
conjuncts (identical to the global wrapper's body, adapted to use
IsCharacteristicFlowOn's initial-condition clause).
This is the packaging layer; the substantive PDE proof lives in
vlasovSolutionViaPushforward_isVlasovSolutionOn above.
Integration smoke test #
A small theorem demonstrating that the three OT files compose: given
two characteristic flows on the same initial probability measures
with finite first moment, the Wasserstein-1 distance between the
pushed-forward measures at time t is bounded by the infimum (over
couplings of the initial measures) of the pushed-forward edist
cost.
This is exactly the shape the USC and derivBound closures in
LeanPool/Vlasov/Basic.lean need: it turns a coupling at time 0 into a
W₁-upper-bound at time t. The Gronwall-on-the-joint-ODE step (which
controls the cost growth) is the next piece — orthogonal to OT,
sits in the dynamics layer.
The theorem is a direct application of wasserstein1_pushforward_le_iInf
from Coupling.lean; the integration test confirms the type chain
composes correctly when the maps are characteristic flows.
Banach fixed-point scaffolding for vlasovWellPosedness #
The sup-W₁ pseudodistance between two curves of measures over a set of
times S. Returns ⨆ t ∈ S, wasserstein1 (ρ t) (σ t) in ℝ≥0∞.
- Symmetric (
supW1On_comm) and satisfies the triangle inequality (supW1On_triangle). - Finite (≠ ⊤) when both curves are
VlasovMeasureCurves on[0, T]with the same moment bound, viasupW1On_ne_top_of_VlasovMeasureCurve.
Used as the contraction metric for the Picard iteration.
Equations
- Vlasov.supW1On S ρ σ = ⨆ t ∈ S, Vlasov.wasserstein1 (ρ t) (σ t)
Instances For
Iterated triangle inequality for supW1On over a sequence.
For any sequence x : ℕ → ℝ → Measure (PhysSpace d) and m ≤ n:
supW1On S (x m) (x n) ≤ ∑ k ∈ Ico m n, supW1On S (x k) (x (k+1)).
Generic structural lemma — stated over an arbitrary sequence and time
set S, not specialised to Picard iteration. Downstream consumers (the
Cauchy-from-contraction argument, the forward-iteration continuation, window
uniqueness) compose against this generic form.
The entire proof stays in ENNReal — supW1On is ENNReal-valued, the sum is
in ENNReal, ENNReal addition is well-defined with ⊤ as absorbing element,
so no finiteness side conditions arise. Project to ℝ via .toReal only at
the boundary (or not at all, as in the ENNReal-form Cauchy argument).
Proof: induction on n starting from n = m via Nat.le_induction.
Base case is the empty sum via supW1On_self. Inductive step combines
supW1On_triangle with Finset.sum_Ico_succ_top.
Metric-dependent smallness predicates #
Smallness predicate for the per-ball Picard-Lindelöf flow's ball-geometry constraint.
Defined as (L : ℝ) * T ^ 2 < 1, this is the smallness condition
the per-ball flow's R-selection requires: R · (1 - L·T²) ≥ N(z)
forces R > 0 only when L·T² < 1. It comes from the tight
adaptive-window Picard-Lindelöf geometry + L-Lipschitz fixed-point
analysis, NOT from contraction.
This is kept separate from the supW1On contraction-ratio constraint
LocalSmallnessContraction (below): the two are genuinely independent
mathematical constraints from distinct sub-arguments, so each predicate
stays matched to its own sub-argument.
Equations
- Vlasov.LocalSmallnessPLBuffer L T = (↑L * T ^ 2 < 1)
Instances For
Smallness predicate for the supW1On contraction-ratio constraint.
For Phi_supW1_contraction's output to satisfy q < 1 — the genuine
M-independent contraction ratio — the constraint is
L · (exp((max 1 L)·T) - 1) / (max 1 L) < 1. This comes from Gronwall
on the W₁-based contraction analysis, inherited off
vlasovVectorField_lipschitzWith (the joint phase-space
max(1, L)-Lipschitz constant).
When max(1, L) = 1 the constraint simplifies to L · (exp T - 1) < 1.
Instances For
The curve metric used by the VlasovMeasureCurve Banach iteration:
supW1On (sup of W₁ distances over the time window).
Defined as abbrev so the abbreviation unfolds transparently — proofs that
reference supW1On work against CurveMetric without modification. New
consumers can use CurveMetric directly for explicit metric-agnosticism.
Equations
- Vlasov.CurveMetric S ρ σ = Vlasov.supW1On S ρ σ
Instances For
Admissible Vlasov measure curves on [0, T]: a curve of probability
measures on PhysSpace d with uniform first-moment bound M, pointwise
integrability of ‖·‖, and W₁-continuity at every time in [0, T].
The W₁-continuity field is phrased per-base-point s ∈ [0, T] as
ContinuousWithinAt of t ↦ W₁(ρ s, ρ t).toReal at s (which equals 0 at
t = s). This is strictly stronger than naive ContinuousOn on the diagonal
— it gives the dominator we need for derived convolution continuity
(vlasovMeasureCurve_convCont) and for the Picard limit's bundling.
d is an explicit parameter so that VlasovMeasureCurve d T M is fully
determined at use sites (otherwise NeZero d cannot be resolved from the
non-discriminating real-valued T, M alone).
- ρ : ℝ → MeasureTheory.Measure (PhysSpace d)
The underlying curve of spatial measures,
t ↦ ρ t. - isProb (t : ℝ) : MeasureTheory.IsProbabilityMeasure (self.ρ t)
- hW1Cont (s : ℝ) : s ∈ Set.Icc 0 T → ContinuousWithinAt (fun (t : ℝ) => (wasserstein1 (self.ρ s) (self.ρ t)).toReal) (Set.Icc 0 T) s
Instances For
supW1On of two VlasovMeasureCurves on [0, T] with moment bound M
is bounded by 2M, hence finite.
Combines pointwise wasserstein1_le_moments_sum with iSup_le over the
compact time set.
Convolution continuity in time, derived from the structural
hW1Cont field via norm_convolveFunctionMeasure_sub_le.
For each x ∈ PhysSpace d, the map t ↦ (∇W ∗ ρ_t)(x) is continuous on
[0, T]. Used inside Φ's well-definedness proof to discharge the
convolution-continuity hypothesis of exists_vlasov_characteristicFlow.
Constant extension past [0, T] #
A VlasovMeasureCurve d T M has its structural properties (moment bound,
integrability of ‖·‖, W₁-continuity) only on Icc 0 T.
exists_vlasov_characteristicFlow_global_smallT takes universal-in-t
hypotheses (the proof internally accesses ρ at t ∈ Icc 0 (T + 1) —
see exists_vlasov_trajectory's hbound_local — but the exposed
signature is universal).
The constant-extension wrapper VlasovMeasureCurve.extend produces a
curve on all of ℝ by clamping t to Icc 0 T: extend t := ρ.ρ (clamp t)
where clamp t := max 0 (min t T). Outside Icc 0 T the extended
curve takes the boundary value (ρ.ρ 0 for t < 0; ρ.ρ T for
t > T). This is the canonical mathematical extension — a Vlasov
solution defined on a finite horizon is naturally extended by holding
the endpoint value past the horizon — and it makes the structural
properties hold universally without modifying the flow construction itself.
Discharge of hρ_cont (universal convolveFunctionMeasure continuity)
routes through vlasovMeasureCurve_convCont precomposed with the
continuous clamp via ContinuousOn.comp_continuous.
Clamp t : ℝ to Icc 0 T. Used by VlasovMeasureCurve.extend to
extend a curve from Icc 0 T to all of ℝ.
Equations
- Vlasov.clampToIcc T t = max 0 (min t T)
Instances For
Constant extension of a VlasovMeasureCurve d T M's underlying curve
ρ.ρ from Icc 0 T to all of ℝ. Defined as ρ.ρ composed with the
clamp max 0 (min t T).
For t ∈ Icc 0 T: extend t = ρ.ρ t.
For t < 0: extend t = ρ.ρ 0.
For t > T: extend t = ρ.ρ T.
The extension preserves all structural properties (IsProbabilityMeasure,
moment bound, integrability of ‖·‖) universally in t, and extends
W₁-continuity to convolveFunctionMeasure-continuity universally in t
via clampToIcc_continuous + vlasovMeasureCurve_convCont.
Equations
- ρ.extend t = ρ.ρ (Vlasov.clampToIcc T t)
Instances For
The extended curve is a probability measure at every t : ℝ.
The extended curve has ‖·‖ integrable at every t : ℝ.
Convolution continuity on the extended curve, universal in t.
Composed from vlasovMeasureCurve_convCont (ContinuousOn on Icc 0 T)
with clampToIcc_continuous via ContinuousOn.comp_continuous. This
provides the flow construction's universal hρ_cont hypothesis directly
from a VlasovMeasureCurve's structural fields.
The constant curve at a probability measure with finite first moment is
a valid VlasovMeasureCurve on [0, T] for any T and any moment
bound M ≥ ∫‖y‖dμ₀.
Equations
- Vlasov.constantCurve μ₀ hμ_int hM = { ρ := fun (x : ℝ) => μ₀, isProb := ⋯, hasMoment := hM, yIntegrable := ⋯, hW1Cont := ⋯ }
Instances For
Per-z trajectory existence for small T.
For each z : PhaseSpace d, produces a trajectory γ : ℝ → PhaseSpace d with
γ 0 = z satisfying the Vlasov ODE on Ioo 0 T.
Smallness constraint: L · T² < 1. Comes from exists_vlasov_characteristicFlow's
hR inequality, whose M·T² term has quadratic-in-T growth. Solving
the algebraic constraint per-z yields a finite R(z) and M(z), with the
existence-bound on T driven by L·T² < 1.
The forward-iteration continuation extends to arbitrary T via shifted initial data; the small-T regime here is where the contraction operates.
True global-in-z characteristic flow on a small-T interval.
For L · T² < 1, produces a characteristic flow (charX, charV) defined
for every z : PhaseSpace d (not just z in a ball), satisfying the Vlasov
ODE on Ioo 0 T.
This is the foundation the Φ pushforward construction depends on; the forward-iteration continuation extends to arbitrary T via shifted-initial-data iteration.
Architecture: per-z application of exists_vlasov_characteristicFlow
with z₀ = z, a = 1 (via exists_vlasov_trajectory helper), bundled
into a global flow via Classical.choose. See helper's docstring for the
algebraic R(z), M(z) computation.
Measurability: NOT exposed. The per-z Classical.choose bundling
doesn't propagate continuity-in-z. A measurable variant
(exists_vlasov_characteristicFlow_global_on_ball_measurable) covers
the analogous question for the ball-localized flow; a parallel
_global_smallT_measurable companion can be added when needed.
The pushforward operator Φ and its well-definedness #
The Φ pushforward operator: maps a characteristic flow + initial measure to
the time-indexed pushforward measure on PhysSpace d.
Equations
- Vlasov.Phi charX f₀ t = MeasureTheory.Measure.map (fun (z : Vlasov.PhaseSpace d) => charX t z) f₀
Instances For
Phi charX f₀ t is a probability measure when charX t is AE-measurable
wrt f₀.
Uniform first-moment bound on Phi charX f₀ under a per-z position growth
hypothesis ‖charX t z‖ ≤ C_T · (‖z‖ + 1).
Composes integral_map (which exchanges the pushforward) with the pointwise
growth bound + linearity of integration over f₀.
‖·‖ is integrable wrt Phi charX f₀ t under the growth hypothesis.
W₁ bound on Φ pushforwards via 1-Lipschitz test functions.
For any two time points s, t, the Wasserstein-1 distance between
Phi charX f₀ s and Phi charX f₀ t is bounded by the integral
∫ z, ‖charX s z - charX t z‖ ∂f₀.
Proof strategy (KR-dual direct): for each 1-Lipschitz φ : PhysSpace d → ℝ,
integral_map converts ∫ φ d(charX_·)#f₀ to ∫ z, φ(charX_· z) ∂f₀.
The integral diff is bounded pointwise by ‖charX s z - charX t z‖ (1-Lipschitz
of φ), then by integral monotonicity.
Architectural note: wasserstein1_pushforward_le_iInf (Coupling.lean)
requires endomaps Φ Ψ : α → α. Our charX t : PhaseSpace d → PhysSpace d
is cross-type, so we work directly with the KR-dual sup — cleaner than
re-deriving the coupling theory.
All Integrable.mono' dominator facts are built as named have statements
before the call (no inline ?_). The integrable_map_measure bridge uses
.mpr to handle the g ∘ f ↔ fun z => g (f z) syntactic mismatch.
Used by Phi_hW1Cont to bound W₁(Φ_s, Φ_t) by an integral that DCT controls
as t → s.
DCT step — the integral ∫ z, ‖charX s z - charX t z‖ ∂f₀
tends to 0 as t → s within Icc 0 T.
Combines pointwise continuity t ↦ charX t z (from the flow's HasDerivAt
→ ContinuousAt) with a uniform dominator 2·C_T·(‖z‖+1) (from the per-z
growth bound) via Mathlib's filter-DCT. The dominator integrability is
built as a named have before the DCT call.
W₁-continuity of t ↦ Phi charX f₀ t at every base point s ∈ Icc 0 T.
Composes the W₁ bound (wasserstein1_Phi_le_integral_diff) with the DCT step
(Phi_integral_diff_tendsto_zero) to conclude that
(wasserstein1 (Phi charX f₀ s) (Phi charX f₀ t)).toReal → 0 as t → s.
Full bundling of Φ into a VlasovMeasureCurve.
Given the four hypothesis bundles (measurability, growth, f₀'s integrability,
flow continuity), bundles the three pushforward well-definedness properties +
Phi_hW1Cont into a VlasovMeasureCurve d T M' where M' := C_T · (M_f₀ + 1).
This is the structured output that the contraction estimate and Banach iteration consume.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Measurability of a characteristic flow given Picard-style boundary regularity.
Given a flow (charX, charV) that:
- matches the initial condition at
t = 0, - is continuous in
tonIcc 0 Tfor eachz(i.e. Picard-solution regularity at the boundary), - satisfies the Vlasov ODE in
HasDerivWithinAt-on-Icoform,
we prove that for each t ∈ Icc 0 T, the map z ↦ (charX t z, charV t z)
is Borel-measurable on PhaseSpace d.
Proof strategy (Gronwall on flow difference, via Mathlib's
dist_le_of_trajectories_ODE): the Vlasov vector field is
max(1, L)-Lipschitz uniformly in t (vlasovVectorField_lipschitzWith),
so two trajectories f, g : ℝ → PhaseSpace d starting from z₁, z₂ satisfy
dist (f t) (g t) ≤ dist(z₁, z₂) · exp(max(1, L) · t) for t ∈ Icc 0 T.
This is exp(K·t)-Lipschitz-in-z, hence continuous in z, hence Borel-
measurable.
Why the boundary regularity is taken as hypothesis: the flow
construction's IsCharacteristicFlowOn ... (Ioo 0 T) Set.univ gives
HasDerivAt only on the open interval Ioo 0 T. Mathlib's
dist_le_of_trajectories_ODE requires ContinuousOn on Icc 0 T plus
HasDerivWithinAt on Ico 0 T (closed at the left endpoint). The boundary
regularity at t = 0 is a property of the underlying Picard construction,
not derivable from IsCharacteristicFlowOn alone. The Picard iteration
discharges these hypotheses from the concrete construction.
This is what the Picard construction plugs into the Φ pipeline.
Step 0b — the flow's Lipschitz-in-z bound (open-interval form).
Extracted from charFlow_measurable_via_gronwall_Ioo's internal
h_dist_bound. Given the open-interval flow ODE, the characteristic flow
z ↦ (charX t z, charV t z) is Lipschitz in the initial datum z with
constant exp((max 1 L) · (t − 0)), uniformly for t ∈ [0, T].
Same hypotheses as charFlow_measurable_via_gronwall_Ioo; the conclusion
is the Grönwall distance bound used by both that lemma (to derive
continuity-in-z hence measurability) and the moment-free dominator in
dobrushin_uniqueness_On.
Open-interval variant of charFlow_measurable_via_gronwall.
Identical to charFlow_measurable_via_gronwall except the derivative
hypothesis is on the OPEN interval Set.Ioo 0 T instead of the
half-open Set.Ico 0 T. This matches the regularity that an
IsCharacteristicFlowOn ... (Set.Ioo 0 T) predicate directly produces
(the ODE holds on the open interval, with the endpoints handled by
continuity).
The proof reuses the per-window Grönwall distance bound, but obtains the
t = 0 endpoint distance bound by taking a one-sided limit
s₀ → 0⁺ of the Grönwall bounds on [s₀, t] (each of which only needs
the derivative on Set.Ico s₀ t ⊆ Set.Ioo 0 T), rather than applying
Grönwall directly on [0, t].
Boundary regularity of a global-in-z flow.
Given a flow (charX, charV) produced by
exists_vlasov_characteristicFlow_global_smallT with the open-interval
predicate IsCharacteristicFlowOn ... (Set.Ioo 0 T) Set.univ, this helper
extracts the closed-interval boundary regularity package needed by both
flow_distance_growth_bound_on and charFlow_measurable_via_gronwall:
h_init— the initial-condition clause att = 0,h_cont_Icc— continuity of(charX, charV)(·, z)on the closed intervalIcc 0 T,h_deriv_Ico— HasDerivWithinAt onIco 0 T(closed at the left endpoint).
The open-interval predicate IsCharacteristicFlowOn exposes only the
Ioo-HasDerivAt clause, while flow_distance_growth_bound_on and the
measurability lemma need Icc-ContinuousOn + Ico-HasDerivWithinAt.
The per-ball flow → per-z trajectory → global-in-z chain carries the
closed-interval HasDerivWithinAt-on-Icc 0 T data as a separate
conjunct; this theorem takes it as the explicit hypothesis h_boundary
and transports it into the precise form needed:
h_initfromhflow.1 z (Set.mem_univ z)(initial-condition clause).h_cont_Iccfromh_boundary's HasDerivWithinAt → ContinuousWithinAt → ContinuousOn (joining components viaProd).h_deriv_Icofromh_boundary's HasDerivWithinAt-on-Icc lifted to HasDerivWithinAt-on-Ici at boundary points viamono_of_mem_nhdsWithin(the local-equivalence-of-filters argument).
Single Picard step VlasovMeasureCurve d T M → VlasovMeasureCurve d T M'.
Composes exists_vlasov_characteristicFlow_global_smallT +
characteristicFlow_boundary_regularity + flow_distance_growth_bound_on +
charFlow_measurable_via_gronwall + PhiAsVlasovMeasureCurve into a
single Picard step.
Output bundle (sigma form): the flow + growth constant + bundled
output curve + local pushforward equation on Icc 0 T. Internally,
σ.ρ = Phi charX_clamped f₀ where charX_clamped t := charX (clampToIcc T t);
on Icc 0 T the clamp is the identity so the pushforward equation
holds with the un-clamped charX.
Φ-step landing in the fixed envelope space.
Phi_step produces a flow (charX, charV) against ρ.extend and bundles its
position pushforward into the constant space VlasovMeasureCurve d T (fun _ => C_T·(M_f₀+1)). The constant bound grows with each Φ-iteration (the moment
fixed-point pathology). This wrapper re-bundles the same pushforward into
the fixed envelope space VlasovMeasureCurve d T m, where m is the
canonical Gronwall envelope of gronwall_envelope_exists: because m is
Φ-invariant at the moment level, Φ maps space(m) to itself, so the Picard
sequence stays in one fixed curve space — dissolving the fixed-point in M.
The moment re-bundling is the measure-level data-free escape:
∫‖x‖∂(map (charX t) f₀) ≤ gronwallBound (∫z‖z‖∂f₀) (1+L) (‖gradW 0‖ + L·m t) t
(phi_moment_envelope_le, fed the per-z growth bound Phi_step
exposes) ≤ m t (envelope invariance hm_inv).
Output also exposes the boundary-regularity bundle (as
exists_vlasov_characteristicFlow_global_smallT) so the Picard recursion can
discharge Phi_supW1_contraction's per-z regularity hypotheses at each step.
The envelope's anchor moment is the phase-space ∫z‖z‖∂f₀ (matching the
integral_map initial value), NOT the spatial marginal.
Pointwise Gronwall on flow difference.
Given two characteristic flow trajectories γ_ρ, γ_σ : ℝ → PhaseSpace d
starting at the same initial condition z, driven by different measure
curves ρ, σ with supW1On(Icc 0 T) ρ σ ≤ D, the pointwise difference
satisfies a Gronwall-type bound:
‖γ_ρ(t) - γ_σ(t)‖ ≤ gronwallBound 0 K (L · D) t
where K := max(1, L).
Proof strategy (Gronwall on the trajectory-difference function):
- Set
f(s) := γ_ρ(s) - γ_σ(s). Thenf(0) = 0(both start atz). f'(s) = vlasovVectorField gradW ρ s (γ_ρ s) − vlasovVectorField gradW σ s (γ_σ s).- Split via triangle:
f'(s) = [VF_ρ γ_ρ − VF_ρ γ_σ] + [VF_ρ γ_σ − VF_σ γ_σ] - First bracket bounded by
K · ‖γ_ρ - γ_σ‖ = K · ‖f s‖viavlasovVectorField_lipschitzWith. - Second bracket: the velocity components cancel (
VF's first component isz.2, identical in both); only the force components differ. Bounded byL · W₁(ρ_s, σ_s).toReal ≤ L · Dvianorm_convolveFunctionMeasure_sub_le. - Apply
norm_le_gronwallBound_of_norm_deriv_right_lewithδ := 0,K := max(1, L),ε := L · D.
Boundary regularity identical to charFlow_measurable_via_gronwall:
ContinuousOn (Icc 0 T) + HasDerivWithinAt on Ico 0 T for each
trajectory. The Picard construction discharges these hypotheses.
Used by the main contraction lemma to bound
supW1On(Icc 0 T)(Phi ρ)(Phi σ) by K_contract(T) · supW1On(Icc 0 T) ρ σ
where K_contract(T) := (L/K) · (exp(K·T) - 1) → 0 as T → 0.
W₁ pushforward bound for two arbitrary maps.
Generalizes wasserstein1_Phi_le_integral_diff (which handled a single
flow at two times) to two arbitrary maps f, g : PhaseSpace d → PhysSpace d.
For pushforwards of the same initial measure f₀:
W₁(f_# f₀, g_# f₀) ≤ ENNReal.ofReal (∫ z, ‖f z - g z‖ ∂f₀).
Proof structure parallel to wasserstein1_Phi_le_integral_diff: KR-
dual direct, with integral_map converting pushforward integrals + the
1-Lipschitz bound |φ y - φ y'| ≤ ‖y - y'‖. Dominators are built as named
haves, and the _map_measure family is bridged via .mp/.mpr.
Used by Phi_pointwise_contraction (below) with
f := charX_ρ t, g := charX_σ t to bound the pushforward W₁ in terms of
the pointwise flow difference.
Pointwise contraction estimate at time t.
Composes the pointwise Gronwall (flow_difference_gronwall_bound)
with the W₁ pair bound to get:
(wasserstein1 (charX_ρ t # f₀) (charX_σ t # f₀)).toReal ≤ gronwallBound 0 K (L·D) t
for t ∈ Icc 0 T, where K := max(1, L) and D := supW1On(Icc 0 T) ρ σ.
Proof: the pointwise Gronwall gives
‖charX_ρ t z - charX_σ t z‖ ≤ gronwallBound 0 K (L·D) t
uniformly in z. Integrating over f₀ (a probability measure) gives the same
bound on ∫ ‖charX_ρ t z - charX_σ t z‖ ∂f₀. The W₁ pair bound then
transfers to the Wasserstein side.
Taking sup over t ∈ Icc 0 T derives the contraction
supW1On(Phi_ρ)(Phi_σ) ≤ K_contract(T) · D where
K_contract(T) := (L/K)·(exp(K·T)−1) → 0 as T → 0.
sup-W₁ contraction estimate over Icc 0 T.
Combines the pointwise contraction (Phi_pointwise_contraction) with
gronwallBound's monotonicity in t to derive:
(supW1On(Icc 0 T) Phi_ρ Phi_σ).toReal ≤ gronwallBound 0 K (L·D) T
where K := max(1, L) and D := supW1On(Icc 0 T) ρ σ bound.
For the Banach fixed-point: expanding gronwallBound's explicit
form (ε/K)·(exp(K·t) − 1), the bound is (L·D/K) · (exp(K·T) − 1) = D · K_contract(T) where K_contract(T) := (L/K)·(exp(K·T) − 1) → 0 as
T → 0. This is the contraction factor the Banach iteration exploits.
Metric-dependence note:
The contraction factor K_contract(T) := (L/K)·(exp(K·T) − 1) is
exponential in T. For contraction (K_contract < 1), this requires
L · (exp T - 1) < 1 when K = 1 — exactly the
LocalSmallnessContraction L T predicate. This is genuinely independent
of the per-ball Picard-Lindelöf flow's quadratic-in-T ball-geometry
constraint LocalSmallnessPLBuffer L T := L·T² < 1; the two predicates
match the two distinct sub-arguments.
Under the Wbar refactor (Dobrushin 1979, §5), the contraction factor
becomes C₂(L) · T — linear in T, no exponential.
LocalSmallnessContraction would reduce to C₂(L) · T < 1;
LocalSmallnessPLBuffer is independent of that change.
Picard-iteration geometric bound.
Given a sequence with geometric contraction supW1On (x k) (x (k+1)) ≤ ENNReal.ofReal (q^k * D₀) for 0 ≤ q < 1, the iterated triangle
inequality + ENNReal.ofReal_sum_of_nonneg + Mathlib's geom_sum_Ico_le_of_lt_one
gives:
supW1On (x m) (x n) ≤ ENNReal.ofReal (D₀ * q^m / (1 - q)) for m ≤ n.
The argument is pure ENNReal modulo one cleanly-localized ENNReal.ofReal
boundary at the bridge between the structural argument (supW1On in ENNReal)
and the closed-form algebra (real geometric series). The Finset partial sum
bound comes from Mathlib/Algebra/Order/Field/GeomSum.lean's
geom_sum_Ico_le_of_lt_one — no case-split on q = 0 vs q > 0 needed,
no shifting tricks via Finset.sum_Ico_eq_sum_range.
Picard iteration is Cauchy from contraction.
Standard Banach-fixed-point Cauchy condition derived from the geometric contraction.
Output form matches exists_wasserstein1_limit_of_cauchy's ENNReal-form
Cauchy hypothesis: for every ε : ENNReal with 0 < ε, there is N such
that supW1On (x m) (x n) < ε for all m, n ≥ N.
Proof sketch: for the symmetric case (m > n), use supW1On_comm.
For ε = ⊤, any N works. For ε < ⊤, pick N such that
D₀ * q^N / (1-q) < ε.toReal; combine with the geometric bound.
Pointwise W₁ bounded by supW1On.
For t ∈ S, the per-t Wasserstein-1 distance is bounded by the sup-W₁
over S. Routine le_iSup chain. Mirror image of the supW1On-shape
lemmas (supW1On_triangle, supW1On_self) — the per-point extraction
from the sup.
Uniform-in-t W₁-tendsto from supW1On Cauchy + per-t
pointwise W₁-tendsto.
Given a sequence x n : ℝ → Measure (PhysSpace d) Cauchy in supW1On S and
per-t pointwise W₁-tendsto to y t, the convergence is uniform in t ∈ S:
for every ε : ENNReal with 0 < ε, there is N such that
wasserstein1 (x n t) (y t) ≤ ε for all n ≥ N and t ∈ S.
Proof idea: triangle through x m t for arbitrarily large m:
wasserstein1 (x n t) (y t) ≤ wasserstein1 (x n t) (x m t) + wasserstein1 (x m t) (y t).
The first term ≤ supW1On (x n) (x m) < ε by Cauchy; the second → 0 by
pointwise tendsto. Apply ENNReal.le_of_forall_pos_le_add for the limit
passage.
Bundle the Picard iteration's W₁-limit as a VlasovMeasureCurve.
Given a sequence of VlasovMeasureCurve d T M iterates with the geometric
contraction property supW1On (x k) (x (k+1)) ≤ ofReal (q^k * D₀),
produce a limit ρ_lim : VlasovMeasureCurve d T M such that
wasserstein1 ((x n).ρ t) (ρ_lim.ρ t) → 0 pointwise (and, by the helper
picard_iterate_limit_uniform_tendsto, uniformly) in t ∈ Icc 0 T.
Proof strategy:
- Apply
picard_iterate_isCauchy_of_contractionto get supW1On Cauchy. - Per-
t ∈ Icc 0 T, the pointwise sequencen ↦ (x n).ρ tis Cauchy in W₁ (bywasserstein1_le_supW1Onfrom the sup-Cauchy). - Invoke
exists_wasserstein1_limit_of_cauchyper-tto obtain the pointwise limitρ_lim t(with probability, integrability, moment bound, W₁-tendsto, all from the strengthened placeholder). - Extend
ρ_limto all ofℝby(x 0).ρoutsideIcc 0 T(so theisProbfield — universal int— holds). - Verify the four
VlasovMeasureCurvefields:isProb: from the placeholder (insideIcc 0 T) +(x 0).isProb(outside).hasMoment: from the placeholder's strengthened moment-preservation conjunct (∫‖y‖ ∂μ ≤ M).yIntegrable: from the placeholder.hW1Cont: ε/3 triangle throughx N, usingpicard_iterate_limit_uniform_tendstofor the uniform tendsto +(x N).hW1Contfor the middle term.