Weak ⟹ Lagrangian: every weak Vlasov solution is transported by its characteristic flow #
(tex: thm:weak-lagrangian)
The forward direction — a Lagrangian solution is weak — is immediate
(IsLagrangianVlasovSolution.1; the substantive pushforward-solves-weak content is
vlasovSolutionViaPushforward_isVlasovSolutionOn, CharacteristicFlow.lean). This file builds
the converse: under the strengthened assumption AssW2 (W ∈ C², see Basic.lean), every
weak Vlasov solution on a window [0,T] is Lagrangian — i.e. it is the pushforward of its
initial datum under the characteristic flow it generates. This is the superposition /
probabilistic-representation principle for the phase-space continuity equation
∂_t f + div_{(x,v)}(b_f · f) = 0 with the Lipschitz field
b_f(t,x,v) = (v, −(∇W ∗ ρ_t)(x)), ρ_t = spatialMarginal (f t).
It upgrades the project's uniqueness from "unique Lagrangian solution" to "unique weak (PDE)
solution". The marquee vlasovWellPosedness / dobrushin are untouched and stay at AssW.
Strategy (three ingredients) #
Freeze the field at ρ^f_t := spatialMarginal (f t) (the field
vlasovVectorField gradW ρ t z = (z.2, −(∇W ∗ ρ_t)(z.1)) is already parametric in ρ). Let
g_t := (Φ_t)_# (f 0) be the pushforward along the flow Φ of this frozen field. Then f
and g solve the same linear continuity equation with the same datum, so f = g, and g is
Lagrangian by construction.
- Flow existence for the frozen
ρ^f— reuseexists_vlasov_characteristicFlow_global_smallT. - Pushforward solves the frozen linear weak eq — reuse the generic helpers SC.1–SC.4
(
vlasov_traj_chain_ruleetc., stated over an arbitraryρ) atρ := ρ^f, bypassing the self-consistent wrappervlasovSolutionViaPushforward_isVlasovSolutionOn. - Linear continuity-equation uniqueness
f = g— the crux (absent from Mathlib). Dual transported test functionψ_s(z) := φ(Φ_{s→T}(z)):s ↦ ∫ ψ_s dμ_sis constant (the∂_sψ + ⟨b,∇ψ⟩ = 0cancellation), so∫φ dμ_T = ∫ψ_0 dμ_0, equal forfandg(sharedμ_0); ranging overφgivesf T = g T.
Decomposition roadmap (sub-lemmas added per build-layer) #
Setup layer (C1):
- #1
vlasov_frozenField_pushforward_isWeakSolOn—gsolves the frozen linear weak eq onIoo 0 T; recompose SC.1 + SC.2 atρ := ρ^f. - #2
exists_frozenField_charFlow_On— instantiateexists_vlasov_characteristicFlow_global_smallTatρ := ρ^f, discharging the integrability / continuity / moment hypotheses.
Final-step layer (C2, crux-independent):
- #7
transportedIntegral_const_On— zero derivative onIoo+ContinuousOnonIcc⟹ const. - #9
measure_eq_of_forall_Cc_integral_eq—∫φ dμ = ∫φ dνfor allC_c^∞ φ⟹μ = ν, via smooth approximation +ext_of_forall_integral_eq_of_IsFiniteMeasure(cf.Wasserstein.lean).
Crux layer (C3):
- #3
charFlow_hasFDerivAt_in_initialPoint— the variational equation:z ↦ Φ_{s→T}(z)is C¹ (HasFDerivAt), derivative solvingM' = (D_z b)·M. Sub-steps: 3.1 variational-ODE existence / uniqueness, 3.2 joint(t,z)continuity, 3.3 difference-quotiento(‖h‖)via Gronwall (the heart), 3.4 assembleHasFDerivAt→ C¹. NeedsAssW2.gradContDiff. - #4
weakSolOn_test_C1c_of_Cinftyc— extendIsVlasovSolutionOn's test class fromC_c^∞toC¹_c(mollification + DCT), sinceψ_s = φ∘Φ_{s→T}is onlyC¹_cwith a C¹ flow. - #5
transportedTestFunction_props—ψ_sisC¹, compactly supported, with∂_sψ_s + ⟨b,∇ψ_s⟩ = 0. - #6
transportedIntegral_hasDerivWithinAt_zero—s ↦ ∫ ψ_s dμ_shas zero derivative onIoo 0 Tfor bothμ = fandμ = g.
Assembly (C4):
- #8
finalTime_integral_eq_of_weak— combine #7 forfandg⟹∫φ df_T = ∫φ dg_T∀C_c^∞ φ. - #10 the top theorem below — package
g's flow witness +f = gintoIsLagrangianVlasovSolutionOn.
Universal (non-_On) form via window-gluing is a deferred follow-on (C5).
Linear (external-field) weak Vlasov solutions #
The self-consistent weak predicate IsVlasovSolutionOn drives the convolution field by the
solution's own spatial marginal. For the superposition argument we need the linear
version, where the field is driven by an external (frozen) measure curve ρ — both the given
weak solution f (with ρ := spatialMarginal ∘ f) and the pushforward g along the
frozen-field flow solve the same IsLinearVlasovSolutionOn gradW ρ · T, and uniqueness for it
(the crux, C3) forces f = g.
Linear weak Vlasov evolution on Ioo 0 T for a test function φ, with the convolution field
driven by an external measure curve ρ (frozen), not the solution's own spatial marginal.
The self-consistent WeakEvolutionEqOn gradW μ φ … (fun _ => 0) T is the special case
ρ = spatialMarginal ∘ μ (modulo the + 0 remainder term).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A measure curve μ solves the linear Vlasov equation on [0,T] driven by the external
field ρ: the distributional identity LinearWeakEvolutionEqOn holds for every C_c^∞ test
function. Mirror of IsVlasovSolutionOn with the field externalized.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A self-consistent weak solution is a linear solution driven by its own spatial marginal.
The two differ only by WeakEvolutionEqOn's + (fun _ => 0) t = + 0 remainder.
C1 #1 — pushforward solves the frozen linear weak equation.
For a characteristic flow (charX, charV) solving the ODE with an external field ρ on
Ioo 0 T, the pushforward g := (charX t, charV t)_# f₀ solves the linear Vlasov equation
driven by that same ρ. Proof: the generic SC.1–SC.3 machinery (change of variables +
chain rule + differentiation-under-the-integral, all parametric in ρ) recomposed at this ρ,
with SC.4's push-back inlined as integral_map (SC.4's packaged form hard-codes the
self-consistent marginal). This is vlasovSolutionViaPushforward_isVlasovSolutionOn with ρ
left free — the _hself self-consistency hypothesis is unused.
C1 #2 — characteristic flow for a frozen field from window data (L11 clamp).
Build the characteristic flow for the given external curve ρ on Ioo 0 T (with boundary
regularity), from probability/moment/integrability/continuity data on the window [0,T] only.
exists_vlasov_characteristicFlow_global_smallT demands universal-in-t instances; we clamp
t ↦ ρ (max 0 (min t T)) into the window (L11), apply the universal producer to the clamped
curve, and transfer on [0,T] where the clamp is the identity.
Final-step layer (crux-independent): constancy + measure extensionality #
C2 #7 — constancy from a vanishing derivative.
If a real function is continuous on [0,T] and has zero derivative throughout the open
interval, its endpoint values agree. This is the dual argument's payoff step: s ↦ ∫ ψ_s dμ_s
is constant, so its value at T (= ∫ φ dμ_T) equals its value at 0 (= ∫ ψ_0 dμ_0). Mean
value theorem (exists_hasDerivAt_eq_slope).
C2 #9 — C_c^∞ test functions determine a finite measure.
If ∫ φ dμ = ∫ φ dν for every smooth compactly-supported φ, then μ = ν (finite measures on
phase space). The dual argument yields equality of integrals against the IsVlasovSolution test
class C_c^∞; this closes the bridge's final step f T = g T. Route: extend C_c^∞ →
bounded-continuous (smooth approximation), then the in-house bounded-continuous extensionality
ext_of_forall_integral_eq_of_IsFiniteMeasure (cf. Wasserstein.lean).
Convenience extractor: under [AssW2 W], a gradient field gradW= ∇W is C¹.
AssW2.gradContDiff gives ContDiff ℝ 1 (fun x => fderiv ℝ W x); composing with the (smooth,
linear) Riesz isometry gradient W x = (toDual ℝ _).symm (fderiv ℝ W x) and rewriting by hgradW
yields ContDiff ℝ 1 gradW.
Crux layer (C3): the variational equation and the dual-transport assembly #
The two interfaces below were the load-bearing pieces of the bridge — both now proven and
axiom-clean. #3 was the genuine research gap (C¹ dependence of an ODE flow on its initial point
— absent from Mathlib), closed via route (b) (difference-quotient + Gronwall); #8 is the
bridge-specific dual-transported-test-function assembly that consumes it. #10 (the public
theorem) composes the reuse layer (exists_frozenField_charFlow_On, #2) with #8.
The dual-argument internals #4/#5/#6 (test-class enlargement C_c^∞ → C¹_c, the
transported test function ψ_s = φ ∘ Φ_{s→t} and its transport identity, and the zero-derivative
of s ↦ ∫ ψ_s dμ_s) are realized against the two-time-flow representation Φ_{s→t} = Φ_t ∘ Φ_s⁻¹
and proven below (weakEvolution_test_C1c_On, transportedTest_transport_identity,
transportedIntegral_hasDerivAt_zero).
C3 F1 — the convolution force field is C¹ in space (Fréchet derivative under the
integral). For gradW ∈ C¹ (and L-Lipschitz, a probability measure ρ with the kernel
integrable), x ↦ ∫ y, gradW (x − y) ∂ρ is Fréchet-differentiable with derivative
∫ y, fderiv ℝ gradW (x₀ − y) ∂ρ. This is the field-regularity foundation of the variational
equation (#3): it makes D_z (vlasovVectorField …) exist and continuous, so the variational ODE
M' = (D_z b)·M has continuous coefficients.
Differentiation under the integral sign (hasFDerivAt_integral_of_dominated_loc_of_lip): the
per-fibre map x ↦ gradW (x − y) is L-Lipschitz (a uniform, integrable bound against a
probability measure) and differentiable, so the parametric integral differentiates with derivative
the integral of the fibrewise derivatives.
C3 F2 — the Vlasov field is C¹ in the phase-space variable, with the block Jacobian.
At fixed time t, vlasovVectorField gradW ρ t = fun (x,v) ↦ (v, −conv(x)) is
Fréchet-differentiable in z = (x,v) with derivative the block continuous-linear map
δ ↦ (δ.2, −(D_x conv)(δ.1)), where D_x conv = ∫ y, fderiv ℝ gradW (z.1 − y) ∂(ρ t) (F1).
This is the coefficient A(t) := D_z b(t, Φ_t z) of the variational ODE M' = A(t)·M.
C3 F1c — the convolution derivative is continuous in space. x ↦ ∫ y, fderiv ℝ gradW (x − y) ∂ρ (the Fréchet derivative of the convolution field, F1) is continuous, by dominated
convergence: the integrand is continuous in x and bounded by ‖fderiv gradW‖ ≤ L (a constant,
integrable against the probability measure ρ). Continuity of the variational coefficient
A(t) in its spatial argument — half of the t-continuity of A (the other half is the
measure-curve regularity t ↦ ρ t, supplied at the V1c ODE-existence step).
Picard iterates for the linear IVP x' = 𝒜(t)x, x(0)=x₀ (the V1c engine):
I₀ ≡ x₀, I_{n+1}(t) = ∫₀ᵗ 𝒜(s)(Iₙ(s)) ds.
Equations
- Vlasov.picardIter 𝒜 x₀ 0 x✝ = x₀
- Vlasov.picardIter 𝒜 x₀ n.succ x✝ = ∫ (s : ℝ) in 0..x✝, (𝒜 s) (Vlasov.picardIter 𝒜 x₀ n s)
Instances For
C3 V1c-engine — the Picard iterates are continuous and satisfy the geometric
(Kt)ⁿ/n!-bound on [0,T]. Proved by simultaneous induction (continuity feeds
integrability, which feeds the next bound). This Σ (KT)ⁿ/n! = e^{KT}-summable bound is the
convergence driver for the V1c fixed point.
C3 V1c-conv — the Dyson sum M := ∑ₙ Iₙ is continuous on [0,T]. Weierstrass M-test:
the terms are dominated by the summable majorant (KT)ⁿ/n!·‖x₀‖, so the series converges
uniformly; the uniform limit of the continuous partial sums is continuous. (M is the candidate
solution: M = x₀ + ∫₀ᵗ 𝒜(s)(M s) ds, proved next.)
C3 V2-core — the Dyson sum is continuous in a PARAMETER (the V2 ingredient). If the
coefficient family 𝒜 : Z → ℝ → (E →L E) is jointly continuous in (z, s) (globally) and
uniformly K-bounded on [0,T] (with x₀ constant in z), then z ↦ ∑ₙ Iₙ(z)(t) is continuous
for each fixed t ∈ [0,T]. This is the parameter analogue of picardSum_continuousOn: each
iterate z ↦ Iₙ(z)(t) is continuous (joint (z,s)-continuity, by induction through the parametric
primitive continuous_parametric_primitive_of_continuous), and the M-test majorant (KT)ⁿ/n!·‖x₀‖
is z-independent, so the uniform-in-z limit of continuous maps is continuous. This is what
makes the variational fundamental matrix z ↦ M z t continuous (V2) — the property the abstract
exists_fundamentalMatrix + choose cannot supply (the choose'd witness is an arbitrary
fiberwise section; see lesson L14).
Window version of picardSum_continuous_param: only joint continuity ON [0,T] is needed.
The coefficient is clamped into [0,T] (projIcc, L11) so the global parametric-primitive lemma
applies, then transferred back by agreement of the iterates on [0,T] (they only integrate over
[0,t] ⊆ [0,T]). This is the form the variational coefficient A(s,z) = D_z b(s, Φ_s z) needs —
it is jointly continuous only on the window [0,T] (the flow Φ_s z is).
C3 V1c-rec — finite Picard recurrence. The (N+1)-th partial Dyson sum equals
x₀ + ∫₀ᵗ 𝒜(s)(Sₙ(s)) ds, where Sₙ = ∑_{n<N} Iₙ. Only finite-sum swaps
(integral_finsetSum, map_sum); no infinite interchange. Passing N → ∞ against the
uniform convergence (picardSum_continuousOn's M-test) yields the integral equation for M.
C3 V1c-inteq — the Dyson sum solves the integral equation.
M(t) = x₀ + ∫₀ᵗ 𝒜(s)(M s) ds on [0,T], where M = ∑'ₙ Iₙ. Pass N → ∞ in the finite
recurrence: LHS → M t (partial sums of the summable series); RHS via DCT (the terms
𝒜(s)(S_N s) → 𝒜(s)(M s) pointwise, dominated by the constant K·∑'ₙ (KT)ⁿ/n!·‖x₀‖).
C3 V1c — existence for a linear ODE with continuous coefficients on a compact interval (the fundamental solution of the variational equation; a Mathlib gap).
For a continuous family of bounded linear maps 𝒜 : ℝ → (E →L[ℝ] E) on a Banach space E, the
linear IVP x' = 𝒜(t) x, x(0) = x₀ has a solution on [0,T]. Generic and reusable
(promotable to Mathlib/Analysis/ODE/); instantiated for the variational equation with
E := PhaseSpace d →L[ℝ] PhaseSpace d, 𝒜(t) := (·).comp-by A(t) (left composition), x₀ := id
to produce the fundamental matrix M(t), where A(t) = vlasovVectorField_hasFDerivAt_in_z's
block CLM evaluated along the flow.
Why not Mathlib's IsPicardLindelof: that needs a globally bounded field
(norm_le : ‖f t x‖ ≤ L); the linear field x ↦ 𝒜(t) x is unbounded, and confining to a ball
makes the Picard window-condition K·e^{KT}·T ≤ e^{KT}−1 fail for a single window (⇒ tiling).
Proof plan (integral-operator contraction, no tiling): on the Banach space
C([0,T]; E) the Picard operator 𝒯[M](t) := x₀ + ∫_0^t 𝒜(s) (M s) ds is K·T-Lipschitz
(K := sup_{[0,T]} ‖𝒜‖, finite by continuity on the compact [0,T]), and its n-th iterate is
(K·T)^n/n!-Lipschitz (induction on the Bochner-integral bound), which is < 1 for large n;
so 𝒯 has a unique fixed point by the iterated-contraction Banach theorem
(ContractingWith + exists_fixedPoint, Mathlib/Topology/MetricSpace/Contracting.lean).
Differentiating the fixed-point integral equation (FTC, HasDerivWithinAt of t ↦ ∫_0^t …)
recovers x' = 𝒜(t) x; x(0) = x₀ from the lower integral limit.
C3 V1c→matrix — the fundamental matrix of a linear ODE. Specialising
exists_linearODE_solution_Icc to the operator space E := F →L[ℝ] F with 𝒜(s) := A(s) ∘ (·)
(left composition) and x₀ := id gives the fundamental solution M' = A(t)∘M, M(0) = id.
This M(t) is the candidate Dflow t z of the variational equation (#3), once A is the Vlasov
field Jacobian A(s) = D_z b(s, Φ_s z) along the flow (F2).
C3 A-cont — the variational coefficient A(s,z) = D_z b(s, Φ_s z) is continuous in s.
A(s,z) is the F2 block CLM (snd).prod(−(∫ fderiv gradW (charX s z − y) ∂ρ_s) ∘ fst); its only
s-varying part is the convolution-derivative integral, continuous via hρD_cont composed with
the flow. The block CLM is reassembled with inl∘snd + inr∘(·) (Mathlib has no clm_prod
continuity combinator). This ContinuousOn is the coefficient input to exists_fundamentalMatrix
that produces the fundamental matrix M_t(z) = Dflow t z for #3.
C3 D1 (Jacobian). The phase-space Jacobian A(s, p) = D_w b(s, p) of the frozen Vlasov
field at the base point p: the block continuous-linear map δ ↦ (δ.2, −(D_x conv ρ_s)(p.1)·δ.1),
where D_x conv ρ_s (p.1) = ∫ y, fderiv ℝ gradW (p.1 − y) ∂ρ_s (F1). This is the coefficient of
the linear variational ODE M' = A(s, Φ_s z)·M; vlasovVectorField_hasFDerivAt_in_z (F2) says it
is the Fréchet derivative of vlasovVectorField gradW ρ s at p.2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
C3 D1a — the uniform-over-compact first-order Taylor remainder of the Vlasov field.
For a fixed initial point z, the first-order remainder of the frozen field b(s,·) at the moving
base point Φ_s z := (charX s z, charV s z),
R(s,w) = b(s,w) − b(s,Φ_s z) − A(s,Φ_s z)·(w − Φ_s z), is o(‖w − Φ_s z‖) uniformly in
s ∈ [0,T]: for every η > 0 there is a single δ > 0 (independent of s) with
‖R(s,w)‖ ≤ η·‖w − Φ_s z‖ whenever ‖w − Φ_s z‖ ≤ δ.
This uniformity is the load-bearing analytic core of D1 (the variational-equation difference
quotient): it is what lets Grönwall bound Φ_t(z+h) − Φ_t(z) − M_t(z)·h by o(‖h‖) uniformly
along the trajectory. Proof: the flow image {Φ_s z : s ∈ [0,T]} is compact (continuous image of
[0,T]), A = D_w b is jointly (s,w)-continuous (from hρD_cont), so A is uniformly
continuous on the compact tube Γ = {(s, Φ_s z + e) : s ∈ [0,T], ‖e‖ ≤ 1} (Heine–Cantor); the
mean-value inequality on closedBall (Φ_s z) δ then converts the modulus into the remainder
bound.
C3 (shared) — joint continuity of the Jacobian on Icc 0 T ×ˢuniv (used by V2's
hA_contOn). The block CLM vlasovFieldJacobian is reassembled inl∘snd + inr∘(·) and its
varying part is continuous via hρD_cont.
C3 (shared) — Lipschitz-in-parameter + ContinuousOn-in-time ⇒ jointly ContinuousOn.
A generic upgrade: if G z · is ContinuousOn (Icc 0 T) for each z and z ↦ G z s is
C-Lipschitz uniformly over s ∈ [0,T], then (z,s) ↦ G z s is jointly continuous on
univ ×ˢ Icc 0 T. Used to derive flow joint continuity (z,s) ↦ Φ_s z from
charFlow_lipschitzInZ_via_gronwall_Ioo (Lipschitz-in-z) + per-z continuity in s.
C3 V2 — the explicit fundamental matrix (Route A, lesson L14): the canonical Dyson-series
solution of M' = A(t)·M, M 0 = id, as a function (not a choose-d witness), so its
parameter-regularity is accessible.
Equations
- Vlasov.fundamentalMatrix A t = ∑' (n : ℕ), Vlasov.picardIter (fun (s : ℝ) => (ContinuousLinearMap.compL ℝ F F F) (A s)) (ContinuousLinearMap.id ℝ F) n t
Instances For
fundamentalMatrix A solves the fundamental-matrix IVP on [0,T] (the non-existential form of
exists_fundamentalMatrix; same proof through the picardSum lemmas).
C3 V2 — the fundamental matrix is continuous in a PARAMETER (closes V2 via Route A).
Specialises picardSum_continuous_param_Icc to 𝒜 := compL∘A, x₀ := id; the compL factor is
1-bounded so the K-bound transfers from A.
Step 3 (i) — joint (z,s) continuity of the Dyson sum (global-hypothesis form).
Mirror of picardSum_continuous_param, concluding JOINT ContinuousOn on univ ×ˢ Icc 0 T
instead of per-t continuity in z. The proof reuses the same joint iterate continuity
(hiter_cont on Z × ℝ) and the same (z,s)-independent M-test majorant (KT)ⁿ/n!·‖x₀‖; only
the final tendstoUniformlyOn ranges over univ ×ˢ Icc 0 T. Used to make the variational
fundamental matrix (z,s) ↦ M z s jointly continuous (the partial-derivative continuity the
two-time-flow joint C¹-ness needs).
Step 3 (i) — joint (z,s) continuity of the Dyson sum (window / ContinuousOn-hypothesis
form). Mirror of picardSum_continuous_param_Icc: clamp s into [0,T] (projIcc, L11) so the
global form applies, then transfer back by iterate-agreement on [0,T].
Step 3 (i) — the fundamental matrix is jointly (z,s)-continuous. Joint companion of
fundamentalMatrix_continuous_param; specialises picardSum_continuous_param_Icc_joint to
𝒜 := compL∘A, x₀ := id. This is the partial-z-derivative continuity input to the joint
C¹-ness of the forward flow (s,z) ↦ Φ_s z (Step 3 (iii)).
Generic Grönwall difference-quotient bound (open-interval ODE + s₀→0⁺ limit). Two curves
uh, mh that approximately solve the same linear ODE w' = vlin·w on Ioo 0 T from the same datum
(uh 0 = mh 0), with mh exact and uh's defect uniformly ≤ εf, satisfy
dist (uh t) (mh t) ≤ gronwallBound 0 K εf t. vlin is abstract (kept opaque to avoid unfolding
the heavy vlasovFieldJacobian integral in the Grönwall application).
C3 D1 — the difference-quotient heart of the variational equation.
Given the fundamental matrix Mz of the linear variational ODE M' = A(s, Φ_s z)·M, M 0 = id
(coefficient A = vlasovFieldJacobian), the time-t flow map w ↦ (charX t w, charV t w) is
Fréchet-differentiable at the fixed point z with derivative exactly Mz t.
This is the load-bearing difference-quotient estimate Φ_t(z+h) − Φ_t(z) − Mz t·h = o(‖h‖).
The matrix is threaded as an explicit hypothesis (rather than choose-d) so the proof can use its
ODE/continuity data directly.
Proof plan (route b — Grönwall on the linearisation remainder). Reduce via
hasFDerivAt_iff_isLittleO_nhds_zero + Asymptotics.isLittleO_iff to: ∀ c>0, ∀ᶠ h, ‖Φ_t(z+h) − Φ_t(z) − Mz t·h‖ ≤ c‖h‖. For fixed small h, the two curves u_h(s) := Φ_s(z+h) − Φ_s(z)
(approximate) and m_h(s) := Mz s·h (exact) both solve w' = A(s, Φ_s z)·w from the same datum
h (Φ_0 = id, Mz 0 = id):
m_his exact — its defect is0(its derivative(A·Mz)(s)·h = A(s)·m_h(s)byhMzderiv+HasDerivWithinAt.clm_apply).u_h's defect is the Taylor remainderR(s, Φ_s(z+h)), bounded byη·‖u_h(s)‖(D1a,vlasovField_taylorRemainder_uniform) once‖u_h(s)‖ ≤ δ(η), which holds with‖u_h(s)‖ ≤ exp(K T)·‖h‖(flow Lipschitz-in-z,charFlow_lipschitzInZ_via_gronwall_Ioo) for‖h‖small. Soεf = η·exp(K T)·‖h‖, uniform ins. The frozen field's two-sided ODE holds only onIoo 0 T, so applydist_le_of_approx_trajectories_ODEon[s₀, t](s₀ ∈ Ioo 0 t) and takes₀ → 0⁺(the initial defectdist(u_h s₀, m_h s₀) → 0by continuity), giving‖u_h t − m_h t‖ ≤ gronwallBound 0 K εf t = εf·(exp(K t)−1)/K. Sinceηis arbitrary this iso(‖h‖).K := max 1 Lis the uniform field Lipschitz constant;‖A(s,·)‖ ≤ Kvianorm_fderiv_le_of_lipschitz. (hcontIccis universal in the initial point because thes₀→0⁺limit needs continuity ofΦ_·(z+h), M2.)
C3 #3 — the variational equation (HasFDerivAt of the flow in its initial point).
For the frozen field b(t,·) = vlasovVectorField gradW ρ t with gradW ∈ C¹ (supplied by the
consumer via assW2_contDiff_gradW), the time-t characteristic map
z ↦ (charX t z, charV t z) is Fréchet-differentiable in the initial point z, with a derivative
Dflow t z that is continuous in z (so the flow map is C¹ in z). The derivative solves the
linear matrix variational ODE M' = (D_z b(t, Φ_t z)) · M, M_0 = id.
This was the load-bearing research gap — Mathlib has no C¹-dependence-of-an-ODE-flow-on-its-
initial-condition lemma — now proven (axiom-clean) via route (b)
(charFlow_lipschitzInZ_via_gronwall_Ioo, CharacteristicFlow.lean, is the Lipschitz-in-z
scaffold; Mathlib Gronwall + the vendored IsPicardLindelof confinement are the analytic inputs):
3.1 existence/uniqueness of the continuous matrix solution M_t(z) of the variational ODE
(fundamentalMatrix); 3.2 joint (t,z) continuity of M (fundamentalMatrix_continuous_param);
3.3 the difference-quotient estimate Φ_t(z+h) − Φ_t(z) − M_t(z)·h = o(‖h‖) uniformly on compacts
(Gronwall on the linearization remainder, using gradW ∈ C¹,
charFlow_hasFDerivAt_of_fundamentalMatrix); 3.4 assembled into HasFDerivAt.
The HasFDerivAt/continuity conclusion is route-independent, so this interface is stable; the
universal-t probability instance + force-integrability h_int are the field-regularity inputs
the proof consumes (the window-only application clamps, L11, at the grind).
hρD_cont (joint continuity of the convolution-derivative field). This is the regularity that
makes the variational coefficient A(s,z) = D_z b(s, Φ_s z) continuous in s — its only non-flow
varying part is D_x conv(ρ_s)(x) = ∫ fderiv gradW (x − y) ∂ρ_s, evaluated at the moving point
Φ_s z, so per-x continuity is not enough; joint (s,x)-continuity is needed. Note the
asymmetry with the field: ∫ gradW(x−y) dρ_s gets joint continuity for free (per-x continuity
- uniform Lipschitz-in-
x,convolveFunctionMeasure_lipschitz_in_x), but the derivative field is NOT uniformly Lipschitz inx(that needsW ∈ C³;AssW2gives onlyC²), so its joint continuity must be supplied.
Option-B note (running — eventual extension). hρD_cont is, in the complete theory, NOT a new
assumption: it is derivable from narrow continuity of s ↦ ρ_s (since fderiv gradW is
bounded continuous, ‖·‖ ≤ L), which is in turn derivable from IsVlasovSolutionOn + tightness
(the uniform moment bound) via the standard "C_c^∞-continuity + tight ⟹ narrow-continuity"
upgrade — a self-contained measure-theory lemma not yet in the codebase. We thread it as a
hypothesis (Option A) to unblock the variational-equation grind; folding it into a derived fact
(so the bridge assumes only the weak solution + moments) is the Option-B extension, tracked as
a follow-up.
Step 1 (dual core) — lower Grönwall / anti-Lipschitz bound on the characteristic flow.
For t ∈ (0,T), the flow Φ_t : z ↦ (charX t z, charV t z) satisfies
dist z₁ z₂ ≤ dist (Φ_t z₁) (Φ_t z₂) · exp(K t) (K = max 1 L), i.e. Φ_t is AntilipschitzWith.
This is the keystone of the two-time-flow inverse construction (Step 2): bi-Lipschitz makes Φ_t
injective with closed range and M_t = DΦ_t invertible (no Liouville needed).
Proof: time-reverse the two trajectories on each [s₀,t] ⊆ (0,T) (so they solve
w' = −b_{s₀+t−r}(w), still K-Lipschitz) and apply the existing forward
dist_le_of_trajectories_ODE; take s₀→0⁺. h_deriv2 is the two-sided HasDerivAt on the open
interval, supplied by IsCharacteristicFlowOn.
Step 2a (dual core, generic) — antilipschitz map ⇒ antilipschitz derivative.
If f is antilipschitz and Fréchet-differentiable at x, its derivative f' is antilipschitz
(hence injective) with the same constant. f' u is the limit of slopes n•(f(x+n⁻¹•u)−f x), each
of norm ≥ ‖u‖/C by antilipschitz; pass to the limit. (Mathlib lacks this producer.)
Step 2 (dual core, generic) — global C¹ inverse of an antilipschitz C¹ self-map.
If Φ : E → E (finite-dim) is C¹ (derivative M z at z), antilipschitz, and Lipschitz, then
each M z is invertible, Φ is bijective, and the global inverse Ψ is Lipschitz with
HasFDerivAt Ψ (M (Ψ w))⁻¹ w. No Liouville/Hadamard: open range
(isOpenMap_of_hasStrictFDerivAt_equiv) + closed range (AntilipschitzWith.isClosed_range) ⇒
clopen ⇒ surjective; inverse derivative from HasStrictFDerivAt.to_local_left_inverse.
Step 2 (dual core) — the characteristic flow Φ_t is a C¹ diffeomorphism on (0,T).
Instantiates the generic global-inverse machinery at Φ_t := (charX t, charV t): its derivative
e z (= #3's Dflow t z) is invertible, Φ_t is bijective, and the inverse Ψ is continuous
with HasFDerivAt Ψ (e (Ψ w))⁻¹ w. hanti comes from Step 1
(charFlow_antilipschitzInZ_via_gronwall_Ioo), hlip from the existing upper Grönwall bound
(charFlow_lipschitzInZ_via_gronwall_Ioo), the derivative family from #3.
Step 3 gating lemma (generic) — joint C¹ from continuous partial derivatives on a
ℝ × E domain (Mathlib-absent). A partial s-derivative Ds p at every point (Ds continuous)
plus a partial z-derivative Dz₀ at the base point ⇒ f is Fréchet-differentiable at (s₀,z₀)
with total derivative (h,k) ↦ h•Ds(s₀,z₀) + Dz₀ k. Proof: split the increment into an
s-part (FTC ∫₀ʰ Ds(s₀+u,z₀+k)du ≈ h•Ds₀ by continuity of Ds) and a z-part
(= Dz₀ k + o(k)).
This is the keystone for the joint (s,w) regularity of the two-time flow Φ_{s→t}: the flow's
partials are M_s z (jointly continuous, V2) in z and b_s(Φ_s z) in s.
PR-ABLE (Mathlib upstream candidate). This is a general real-analysis result with no Vlasov
content — "a function on ℝ × E with a continuous partial derivative in the ℝ factor and a
Fréchet partial derivative in the E factor is Fréchet-differentiable" — filling a genuine gap in
Mathlib/Analysis/Calculus. Generalisation worth doing before a PR: replace the ℝ factor by an
arbitrary first factor with an analogous "integrate the partial along segments" hypothesis, and
weaken Continuous Ds to ContinuousAt Ds at the base point (the proof only uses a neighbourhood
of (s₀,z₀)).
Step 3 gating lemma (LOCAL / open-set form) — joint HasFDerivAt from continuous partial
derivatives on an open set U ⊆ ℝ × E. The open-set generalisation of
hasFDerivAt_of_continuous_partials (which is the U := univ special case) that the PR-note above
flagged: the s-partial is required only on U, and Ds only ContinuousOn U. This is the form
the Vlasov flow needs — its partials exist and are continuous only on the open window
Ioo 0 T ×ˢ univ. Proof = the global proof + ball-in-U bookkeeping (B((s₀,z₀),r) ⊆ U; the FTC
segment points (u, z₀+p.2), u ∈ uIcc s₀ (s₀+p.1), lie within ‖p‖ < min δ (r/2) of (s₀,z₀),
hence in U and within the continuity radius δ).
NOTE (consolidation TODO): the global hasFDerivAt_of_continuous_partials above is the univ
special case of this; a follow-up cleanup should rewrite it as the one-line corollary
hasFDerivAt_of_continuous_partials_open isOpen_univ (Set.mem_univ _) (fun p _ => hDs p) hDs_cont.continuousOn hDz₀ to drop the duplicated proof. PR-ABLE (the more
general statement).
Step 3 — the forward flow (s,z) ↦ Φ_s z is jointly continuous on Icc 0 T ×ˢ univ
((s,z)-order). Gronwall Lipschitz-in-z (uniform over [0,T]) + per-z continuity-in-s, via
the generic continuousOn_prod_of_lipschitz_continuousOn, then a prod-order swap. Extracted from
#3's V2-branch pattern so the joint C¹-ness (Step 3 (iii)) can reuse it directly.
Step 3 (ii) — the field along the flow (s,z) ↦ b_s(Φ_s z) is jointly continuous on
Icc 0 T ×ˢ univ. First component charV from flow joint continuity; second component
-(∇W ∗ ρ_s)(charX s z) from (s,x) ↦ (∇W∗ρ_s)(x) jointly continuous (equi-Lipschitz-in-x from
convolveFunctionMeasure_lipschitz_in_x + continuous-in-s from hf_cont) composed with the flow.
This is the partial-s-derivative continuity input to the joint C¹-ness (Step 3 (iii)).
Step 3 (iii) — the forward flow (s,z) ↦ Φ_s z is jointly C¹ on U := Ioo 0 T ×ˢ univ:
Fréchet-differentiable at every point with a jointly-continuous total derivative DΦ. Built by
composing the open-set gating theorem (hasFDerivAt_of_continuous_partials_open) — fed the
s-partial b_s(Φ_s z) (flow ODE, jointly continuous by item (ii)) and the z-partial M_s z
(the fundamental matrix, via D1c, jointly continuous by item (i)). Per L14 the matrix is rebuilt
concretely (fundamentalMatrix (A z) s), NOT routed through #3's existential.
The field bfun and matrix Mfun are made opaque locals (clear_value, the D1c lesson) so the
gating unification stays syntactic and never unfolds the vlasovVectorField/vlasovFieldJacobian
integrals — the per-point derivative facts are established in terms of them before clearing.
A is kept transparent through the D1c call (whose coefficient is
vlasovFieldJacobian) and cleared
only afterwards (before the projection-reduction defeqs). No maxHeartbeats bump needed.
Step 3 (iv-A) — the forward flow (s,z) ↦ Φ_s z is ContDiffAt ℝ 1 at each point of the
open window (the chart-IFT input for item (iv)). Lifts item (iii)'s HasFDerivAt-everywhere +
ContinuousOn-derivative to ContDiffAt via contDiffAt_succ_iff_hasFDerivAt.
Step 3 (iv) — the per-slice inverse Ψ_s := Φ_s⁻¹ is jointly C¹ on Ioo 0 T ×ˢ univ,
the keystone of the two-time flow Φ_{s→t} = Φ_t ∘ Φ_s⁻¹.
PROVEN (axiom-clean) via the space-time chart inverse-function theorem — see the proof plan
below, realized exactly as scouted: charFlow_contDiffAt_joint (iv-A) for the chart ContDiffAt,
the block-triangular ≃L (invertibility from Step 2's e z₀ via HasFDerivAt.unique +
ofBijective), ContDiffAt.to_localInverse, and the global patch via localInverse_unique (the
global per-slice inverse is a local left inverse of the chart, by injectivity on the window).
Per slice s ∈ Ioo 0 T, Step 2 (exists_charFlow_inverse_On) already gives the inverse Ψ_s and
its invertible derivative family e (= M_s z, #3/D1c); here we upgrade to JOINT (s,w)
regularity via the space-time chart.
Proof plan (atoms scouted + verified, 2026-06-16):
- Forward chart
Ξ : (s,z) ↦ (s, Φ_s z)isContDiffAt ℝ 1at each(s₀,z₀) ∈ Ioo 0 T ×ˢ univ.Φ := (charX·, charV·)is jointlyC¹(charFlow_hasFDerivAt_joint, item (iii) —∃ DΦ,HasFDerivAt-everywhere +ContinuousOn DΦ); lift toContDiffAt ℝ 1 ΦviacontDiffAt_succ_iff_hasFDerivAt(Mathlib/.../ContDiff/Defs.lean:994,n := 0: feedDΦ, the open nbhdU ∈ 𝓝,HasFDerivAt-on-U, andContDiffAt 0 DΦfromcontDiffAt_zero+ContinuousOn DΦ U).Ξ = (fst, Φ)soContDiffAt ℝ 1 ΞviaContDiffAt.prodwithcontDiffAt_fst. DΞ(s₀,z₀)is an invertible≃L. Block-lower-triangular(h,k) ↦ (h, h•b + M·k)withb := b_{s₀}(Φ_{s₀}z₀),M := M_{s₀}z₀invertible (Step 2'se₀ z₀). Build theℝ×E ≃L ℝ×EviaContinuousLinearEquiv.ofBijective(inject:(h,k)↦0 ⇒ h=0, thenM k=0 ⇒ k=0; finite-dimLinearMap.injective_iff_surjective).HasStrictFDerivAt Ξ (this ≃L) (s₀,z₀)viaContDiffAt.hasStrictFDerivAt'.- Local
C¹inverse + patch.ContDiffAt.to_localInverse(Mathlib/.../InverseFunctionTheorem/ContDiff.lean:66) ⇒Ξ.localInverseisContDiffAt ℝ 1atΞ(s₀,z₀) = (s₀, Φ_{s₀}z₀). The global(s,w)↦(s, Ψ_s w)agrees withΞ.localInverseon a nbhd (both left-inverses;Ξinjective onIoo 0 T ×ˢ univsincesis preserved + eachΦ_sinjective per Step 2) ⇒ContDiffAt.congr⇒(s,w)↦(s,Ψ_s w)isContDiffAt ℝ 1at each point ⇒ContDiffOn ℝ 1(projecting off thescomponent,ContDiffAt.snd). - Bijectivity is the per-slice
LeftInverse/RightInversefromexists_charFlow_inverse_On, packaged into thes-indexedΨ. The two-time flowΦ_{s→t} = Φ_t ∘ Ψ_sis then jointlyC¹by composing withΦ_t(C¹in its argument,#3), and the dual core's transport identity differentiates it.
Step 4 — the transported test function and the transport identity #
The dual core's s ↦ ∫ ψ_s d(f s) argument rests on the backward-transported test
ψ_s := φ ∘ Φ_{s→t} where Φ_{s→t} = Φ_t ∘ Φ_s⁻¹ is the two-time flow (Step 3 gave it jointly
C¹). Two deliverables, both taking the outputs of Step 3 (the inverse Ψ + the C¹ terminal
map Φ_t) as hypotheses rather than re-deriving them from the flow-construction data:
Step 4 (4a) — the two-time flow Φ_{s→t} = Φ_t ∘ Φ_s⁻¹ is jointly C¹ on
Ioo 0 T ×ˢ univ.
The two-time flow (s,w) ↦ (charX t (Ψ_s w), charV t (Ψ_s w)) is the composition of the terminal
map Φ_t = (charX t ·, charV t ·) (C¹ in its argument — hΦt_C1, from Step 2 / item (iii) at the
fixed time t) with the jointly-C¹ inverse family (s,w) ↦ Ψ_s w (hΨ_C1, item (iv)). Proof:
ContDiff.comp_contDiffOn.
Step 4 (4b) — the transport identity ∂_s ψ_s + Dψ_s · b_s = 0.
For the backward-transported test ψ_s(w) := φ(Φ_t(Ψ_s w)) = φ(Φ_{s→t} w), the partial
s-derivative cancels the spatial directional derivative along the field:
∂_s ψ_s(w) = -(Dψ_s(w))(b_s(w)), where b_s = vlasovVectorField gradW ρ s and
Dψ_s(w) = fderiv ℝ (ψ s) w. This is the dual of vlasov_traj_chain_rule (the pushforward
direction) and the engine that makes s ↦ ∫ ψ_s d(f s) constant in Step 6.
Proof:
ψis jointlyC¹onIoo 0 T ×ˢ univ(4a +φsmooth), soHasFDerivAt (uncurry ψ) Dψ (s,w)at the interior point(s,w), withDψthe joint Fréchet derivative.- Constancy curve: set
z₀ := Ψ_s w, sow = Φ_s z₀(hΨ_right). The composites' ↦ ψ_{s'}(Φ_{s'} z₀) = φ(Φ_t(Ψ_{s'}(Φ_{s'} z₀))) = φ(Φ_t z₀)is constant ins'(hΨ_left:Ψ_{s'} ∘ Φ_{s'} = id), hence has zeros'-derivative. - The curve
c(s') := (s', Φ_{s'} z₀)hasHasDerivAt c (1, b_s w) s(hflow_ode+id), withc(s) = (s, w). Chain rule:0 = Dψ(s,w)(1, b_s w) = Dψ(s,w)(1,0) + Dψ(s,w)(0, b_s w). Dψ(s,w)(1,0) = ∂_s ψ_s(w)(composeuncurry ψwiths' ↦ (s', w)) andDψ(s,w)(0,k) = (fderiv ℝ (ψ s) w) k(compose withw' ↦ (s, w')). Surjectivity (hΨ_right) covers everyw. Rearrange to the claimedHasDerivAt.
Helper 1 — uniform mollification of a continuous, compactly-supported function.
The mollified family ρ_n ⋆ g converges to g uniformly (not just pointwise), the
load-bearing analytic input the C¹_c test-class enlargement (#4) needs. Proof: uniform
continuity of g (compact support) gives a single δ; once rOut_n < δ, the pointwise bump
estimate dist_normed_convolution_le fires at every base point simultaneously.
Helper 2 — the mollified Fréchet derivative converges uniformly.
fderiv (ρ_n ⋆ χ) = ρ_n ⋆ (fderiv χ) (convolution commutes onto the C¹ factor via
HasCompactSupport.hasFDerivAt_convolution_right, with precompR reconciled to lsmul on the
operator codomain), and the right-hand side converges uniformly to fderiv χ by Helper 1 applied
to the continuous, compactly-supported fderiv χ.
Norm bound for the dual-composed difference of two Fréchet derivatives.
Chain rule: the Fréchet derivative of an x-slice is the composition with inl.
Chain rule: the Fréchet derivative of a v-slice is the composition with inr.
Continuity of the first-slot partial-gradient field of a C¹ test function.
Continuity of the second-slot partial-gradient field of a C¹ test function.
Compact support of the first-slot partial-gradient field.
Compact support of the second-slot partial-gradient field.
First-slot partial gradients of two tests differ by at most the full Fréchet-derivative difference.
Second-slot partial gradients of two tests differ by at most the full Fréchet-derivative difference.
Integrability of the weak-evolution integrand against a probability measure: continuous with compact support (both gradient slots), continuous field.
Pointwise bound on the difference of two weak-evolution integrands: on the
common support K it is (R_K + B) * δ (norm bound R_K on K, field bound B
on K, gradient-slot distance δ); off K both integrands agree.
On the window, the frozen convolution field over the spatial marginal is integrable (in force form), linearly bounded, and continuous — packaged for consumers that quantify over the window.
Uniform convergence of integrands implies convergence of the integrals against a probability measure (every term integrable).
Per-z phase-space ODE of a characteristic flow on the open window, in
vlasovVectorField form.
A Fréchet derivative applied to a phase-space vector decomposes as inner products against the two partial-gradient slices.
FTC bound on the linearization remainder of a real function: if F has
derivative D r along the segment and D stays within ε of D s there,
then |F σ − F s − (σ−s)·D s| ≤ ε·|σ−s|.
The transported-integral difference σ ↦ ∫ ψ_σ d(f σ) − ∫ ψ_s d(f σ) has
derivative −Vb = ∫ D d(f s) at s, from a uniform linearization of r ↦ ψ_r
(term T1) and narrow continuity of σ ↦ ∫ D d(f σ) (term T2).
#6a (Step 6, the diagonal chain rule) — s ↦ ∫ ψ_s d(f s) has zero σ-derivative.
The analytic heart of the dual core: for the backward-transported test
ψ_σ(w) := φ(Φ_t(Ψ_σ w)), the diagonal map I(σ) := ∫ ψ_σ d(f σ) (both the integrand and the
measure move with σ) has HasDerivAt I 0 on Ioo 0 t. The two σ-dependencies cancel.
Strategy (the measure f is a bare weak solution, so there is no joint Fréchet structure to lean
on — the two partials are combined by hand):
- Split
I = Bint + qwithBint σ := ∫ ψ_s d(f σ)(integrand frozen ats) andq σ := ∫ (ψ_σ − ψ_s) d(f σ). HasDerivAt Bint Vb svia theC¹_c-extended weak equationweakEvolution_test_C1c_On(#4) tested against the fixedC¹_cfunctionψ_s(this is why #4 had to land first).HasDerivAt q (−Vb) svia the little-o definition: writingDQ_r z := ∂_r ψ_r(z), the remainder splits asT1 + T2whereT1 = ∫ (ψ_σ − ψ_s − (σ−s)·DQ_s) d(f σ)iso(σ−s)by uniform differentiability ofr ↦ ψ_rover a fixed compactK(FTC + Heine–Cantor;Kis the flow image of[a,b] × Ψ_t(tsupport φ)— this is whathflowjointis for: bounding the moving support ofψ_r), andT2 = (σ−s)·(∫ DQ_s d(f σ) − ∫ DQ_s d(f s))iso(σ−s)by narrow continuity (hf_narrow).- The cancellation
Vb = −∫ DQ_s d(f s)comes from the Step-4 transport identity (transportedTest_transport_identity, givingDQ_s = −(fderiv ψ_s)·b_s) composed with the gradient↔fderiv partial decomposition (matching #4's RHS).
C3 #8 (dual-transport core) — ∫ φ d(f t) = ∫ φ∘Φ_t d(f 0) for every C_c^∞ test.
The dual transported-test-function argument showing the weak solution f transports along its
frozen-field characteristics. Fix a terminal t ∈ [0,T] and a C_c^∞ test φ. Let Φ_{s→t}
be the two-time flow (forward from time s to time t along the frozen-field characteristics)
and ψ_s := φ ∘ Φ_{s→t} the backward-transported test (so ψ_t = φ and ψ_0 = φ ∘ Φ_t). Then:
Proven, axiom-clean (this body composes the six leaves below). The two-time flow
Φ_{s→t} = Φ_t ∘ Φ_s⁻¹ is jointly C¹ (Steps 1–4, proven: charFlow_inverse_contDiffOn_joint +
transportedTest_transport_identity). The constancy of I(s) := ∫ ψ_s d(f s) on [0,t] is
assembled by dualCore_main (sorry-free): the if-patched I (the left endpoint s = 0, where
item-(iv) Ψ_s is junk, is set directly to ∫ φ∘Φ_t d(f 0)), endpoint identities
I 0 = ∫ φ∘Φ_t d(f 0) and I t = ∫ φ d(f t) (via the right-inverse Ψ_t), then
transportedIntegral_const_On (#7). t = 0 is trivial (Φ_0 = id); t = T goes through
dualCore_terminal (a t → T⁻ limit).
The constancy rests on six leaves (all proven, axiom-clean):
weakEvolution_test_C1c_On(#4 = Step 5) — the linear weak equation extended from theC_c^∞test class toC¹_c(so it can be tested against the only-C¹ψ_r).vlasovSolutionOn_integral_continuousOn(NC) —s ↦ ∫ G s · d(f s)is continuous for a jointly-continuous, uniformly-compactly-supported familyG(narrow continuity of the weak solution, consumption form; derivable from the weak eq + moments).transportedIntegral_hasDerivAt_zero(#6a) —HasDerivAt I 0onIoo 0 t, the diagonal chain rule:∂_σvia #4 +∂_rvia differentiation-under-the-integral againstf s+ the transport-identity cancellation; assembles via the Step-3 continuous-partials gating theorem.transportedIntegral_continuousOn(#6b) —ContinuousOn I (Icc 0 t), via NC + Step-4 joint continuity (thes → 0⁺endpoint is the load-bearing case).frozenFlow_inverse_On— the item-(iv) discharge producingΨ+ its four facts (L11 clamp for the universal probability instance).dualCore_terminal— thet = Tendpoint.
The pushforward side is integral_map by definition, so the dual argument is needed only for f
(the plan's #1 pushforward-solves-linear lemma is not on this path).
C3 #8 — the weak solution equals its frozen-field pushforward on the window.
f t = (Φ_t)_# (f 0) on [0,T]. Skeleton: measure_eq_of_forall_Cc_integral_eq (#9) reduces
this to per-C_c^∞-test integral equality, and integral_map turns the pushforward side into
∫ φ∘Φ_t d(f 0) — leaving exactly the dual-transport core
weak_eq_frozenField_pushforward_dualCore. Flow measurability on the window (needed by
integral_map and the probability-measure instances) comes from an L11 clamp of ρ^f into
[0,T] + charFlow_measurable_via_gronwall_Ioo.
Weak ⟹ Lagrangian on [0,T] (tex: thm:weak-lagrangian).
Under AssW2 (W ∈ C²) and a per-window smallness, every weak Vlasov solution on [0,T] with
finite first moments (and the ρ-regularity the frozen-field flow construction needs) is the
pushforward of its initial datum under the characteristic flow it generates — i.e. it is
Lagrangian. This is the localized, forward-window form matching vlasovWellPosedness's
architecture; the universal form is obtained by window-gluing (deferred).
Hypotheses mirror what exists_vlasov_characteristicFlow_global_smallT consumes for the frozen
curve ρ^f := fun t => spatialMarginal (f t).
hf_cont_deriv (joint continuity of the convolution-derivative field
∫ fderiv gradW (x−y) ∂ρ^f_s) is the regularity threaded down to the variational equation (#3);
like hf_cont it is assumed at the bridge boundary (Option A). In the complete theory it is
derivable from hf_weak + hf_mom (tightness) via a narrow-continuity upgrade — the Option-B
extension that would let the bridge assume only the weak solution + moments; see #3's docstring.
Proof (complete, axiom-clean; built over C1–C4 per the roadmap above):
freeze the field at ρ^f, build its flow Φ (#2) and the pushforward g := (Φ_t)_# (f 0) which
solves the frozen linear weak eq (#1); show f = g by the dual-transported-test-function
uniqueness (#3–#9, the variational-equation crux); conclude f is Lagrangian (#10).