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.
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.
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.
_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 proof combines flow_distance_growth_bound_on with the flow's local
ODE and a uniform derivative bound for the compactly supported test function.
The global vlasov_trajectory_lipschitz_bound_lag follows by restricting its
flow to a suitable finite interval.
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)).
_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-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.