Characteristic construction and growth bounds #
The phase-space vector field, Grönwall estimates, window predicates and characteristic construction compile before the pushforward and fixed-point arguments that use them.
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.
A Lipschitz force has an affine convolution bound controlled by the first moment.
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.
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.
The global flow_distance_growth_bound follows by supplying its initial
condition, continuity and derivative statements as boundary regularity.
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.
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)).
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.
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.