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.

1. Flow existence for the frozen ρ^f — reuse exists_vlasov_characteristicFlow_global_smallT.
2. Pushforward solves the frozen linear weak eq — reuse the generic helpers SC.1–SC.4 (vlasov_traj_chain_rule etc., stated over an arbitrary ρ) at ρ := ρ^f, bypassing the self-consistent wrapper vlasovSolutionViaPushforward_isVlasovSolutionOn.
3. Linear continuity-equation uniqueness f = g — the crux (absent from Mathlib). Dual transported test function ψ_s(z) := φ(Φ_{s→T}(z)): s ↦ ∫ ψ_s dμ_s is constant (the ∂_sψ + ⟨b,∇ψ⟩ = 0 cancellation), so ∫φ dμ_T = ∫ψ_0 dμ_0, equal for f and g (shared μ_0); ranging over φ gives f T = g T.

Decomposition roadmap (sub-lemmas added per build-layer)

Setup layer (C1):

• #1 vlasov_frozenField_pushforward_isWeakSolOn — g solves the frozen linear weak eq on Ioo 0 T; recompose SC.1 + SC.2 at ρ := ρ^f.
• #2 exists_frozenField_charFlow_On — instantiate exists_vlasov_characteristicFlow_global_smallT at ρ := ρ^f, discharging the integrability / continuity / moment hypotheses.

Final-step layer (C2, crux-independent):

• #7 transportedIntegral_const_On — zero derivative on Ioo + ContinuousOn on Icc ⟹ const.
• #9 measure_eq_of_forall_Cc_integral_eq — ∫φ dμ = ∫φ dν for all C_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 solving M' = (D_z b)·M. Sub-steps: 3.1 variational-ODE existence / uniqueness, 3.2 joint (t,z) continuity, 3.3 difference-quotient o(‖h‖) via Gronwall (the heart), 3.4 assemble HasFDerivAt → C¹. Needs AssW2.gradContDiff.
• #4 weakSolOn_test_C1c_of_Cinftyc — extend IsVlasovSolutionOn's test class from C_c^∞ to C¹_c (mollification + DCT), since ψ_s = φ∘Φ_{s→T} is only C¹_c with a C¹ flow.
• #5 transportedTestFunction_props — ψ_s is C¹, compactly supported, with ∂_sψ_s + ⟨b,∇ψ_s⟩ = 0.
• #6 transportedIntegral_hasDerivWithinAt_zero — s ↦ ∫ ψ_s dμ_s has zero derivative on Ioo 0 T for both μ = f and μ = g.

Assembly (C4):

• #8 finalTime_integral_eq_of_weak — combine #7 for f and g ⟹ ∫φ df_T = ∫φ dg_T ∀ C_c^∞ φ.
• #10 the top theorem below — package g's flow witness + f = g into IsLagrangianVlasovSolutionOn.

Universal (non-_On) form via window-gluing is a deferred follow-on (C5).

theorem Vlasov.charFlow_ode_of_isCharacteristicFlowOn {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (z : PhaseSpace d) (s' : ℝ) : s' ∈ Set.Ioo 0 T → HasDerivAt (fun (s'' : ℝ) => (charX s'' z, charV s'' z)) (vlasovVectorField gradW ρ s' (charX s' z, charV s' z)) s'

Per-z phase-space ODE of a characteristic flow on the open window, in vlasovVectorField form.

theorem Vlasov.fderiv_apply_eq_inner_gradientSlices {d : ℕ} (θ : PhaseSpace d → ℝ) (z : PhaseSpace d) (hθ : DifferentiableAt ℝ θ z) (p q : PhysSpace d) : (fderiv ℝ θ z) (p, q) = inner ℝ p (gradient (fun (x : PhysSpace d) => θ (x, z.2)) z.1) + inner ℝ q (gradient (fun (v : PhysSpace d) => θ (z.1, v)) z.2)

A Fréchet derivative applied to a phase-space vector decomposes as inner products against the two partial-gradient slices.

theorem Vlasov.abs_linearization_remainder_le (F D : ℝ → ℝ) (s σ ε : ℝ) (hderiv : ∀ r ∈ Set.uIcc s σ, HasDerivAt F (D r) r) (hD_cont : ContinuousOn D (Set.uIcc s σ)) (hD_close : ∀ r ∈ Set.uIoc s σ, |D r - D s| ≤ ε) : |F σ - F s - (σ - s) * D s| ≤ ε * |σ - s|

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|.

theorem Vlasov.hasDerivAt_integral_sub_of_uniform_linearization {d : ℕ} (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (ψ : ℝ → PhaseSpace d → ℝ) (D : PhaseSpace d → ℝ) (s a b : ℝ) (hs_ab : s ∈ Set.Ioo a b) (hab_sub : Set.Icc a b ⊆ Set.Ioo 0 T) (hψr_int : ∀ r ∈ Set.Icc a b, ∀ σ ∈ Set.Icc 0 T, MeasureTheory.Integrable (ψ r) (f σ)) (hD_int : ∀ σ ∈ Set.Icc 0 T, MeasureTheory.Integrable D (f σ)) (hunif : ∀ ε > 0, ∀ᶠ (σ : ℝ) in nhds s, ∀ (z : PhaseSpace d), |ψ σ z - ψ s z - (σ - s) * D z| ≤ ε * |σ - s|) (hnarrow : ContinuousWithinAt (fun (σ : ℝ) => ∫ (z : PhaseSpace d), D z ∂f σ) (Set.Icc 0 T) s) (hsIoo : s ∈ Set.Ioo 0 T) (Vb : ℝ) (hVb : Vb = -∫ (z : PhaseSpace d), D z ∂f s) : HasDerivAt (fun (σ : ℝ) => ∫ (z : PhaseSpace d), ψ σ z ∂f σ - ∫ (z : PhaseSpace d), ψ s z ∂f σ) (-Vb) 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).

theorem Vlasov.transportedIntegral_hasDerivAt_zero {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hf_weak : IsVlasovSolutionOn gradW f T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (L : NNReal) (hL : LipschitzWith L gradW) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (φ : PhaseSpace d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (Ψ : ℝ → PhaseSpace d → PhaseSpace d) (hΨ_left : ∀ s ∈ Set.Ioo 0 T, Function.LeftInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_right : ∀ s ∈ Set.Ioo 0 T, Function.RightInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_C1 : ContDiffOn ℝ 1 (fun (p : ℝ × PhaseSpace d) => Ψ p.1 p.2) (Set.Ioo 0 T ×ˢ Set.univ)) (hΦt_C1 : ContDiff ℝ 1 fun (z : PhaseSpace d) => (charX t z, charV t z)) (hflowjoint : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)) (s : ℝ) (hs : s ∈ Set.Ioo 0 t) : HasDerivAt (fun (σ : ℝ) => ∫ (z : PhaseSpace d), φ (charX t (Ψ σ z), charV t (Ψ σ z)) ∂f σ) 0 s

#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 + q with Bint σ := ∫ ψ_s d(f σ) (integrand frozen at s) and q σ := ∫ (ψ_σ − ψ_s) d(f σ).
• HasDerivAt Bint Vb s via the C¹_c-extended weak equation weakEvolution_test_C1c_On (#4) tested against the fixed C¹_c function ψ_s (this is why #4 had to land first).
• HasDerivAt q (−Vb) s via the little-o definition: writing DQ_r z := ∂_r ψ_r(z), the remainder splits as T1 + T2 where T1 = ∫ (ψ_σ − ψ_s − (σ−s)·DQ_s) d(f σ) is o(σ−s) by uniform differentiability of r ↦ ψ_r over a fixed compact K (FTC + Heine–Cantor; K is the flow image of [a,b] × Ψ_t(tsupport φ) — this is what hflowjoint is for: bounding the moving support of ψ_r), and T2 = (σ−s)·(∫ DQ_s d(f σ) − ∫ DQ_s d(f s)) is o(σ−s) by narrow continuity (hf_narrow).
• The cancellation Vb = −∫ DQ_s d(f s) comes from the Step-4 transport identity (transportedTest_transport_identity, giving DQ_s = −(fderiv ψ_s)·b_s) composed with the gradient↔fderiv partial decomposition (matching #4's RHS).

theorem Vlasov.transportedIntegral_continuousOn {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (φ : PhaseSpace d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (Ψ : ℝ → PhaseSpace d → PhaseSpace d) (hΨ_left : ∀ s ∈ Set.Ioo 0 T, Function.LeftInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_right : ∀ s ∈ Set.Ioo 0 T, Function.RightInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_C1 : ContDiffOn ℝ 1 (fun (p : ℝ × PhaseSpace d) => Ψ p.1 p.2) (Set.Ioo 0 T ×ˢ Set.univ)) (hΦt_C1 : ContDiff ℝ 1 fun (z : PhaseSpace d) => (charX t z, charV t z)) (L : NNReal) (hflowjoint : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)) (hanti : ∀ s ∈ Set.Ioo 0 T, ∀ (z₁ z₂ : PhaseSpace d), dist z₁ z₂ ≤ dist (charX s z₁, charV s z₁) (charX s z₂, charV s z₂) * Real.exp (↑(max 1 L) * s)) : ContinuousOn (fun (s : ℝ) => if s = 0 then ∫ (z : PhaseSpace d), φ (charX t z, charV t z) ∂f 0 else ∫ (z : PhaseSpace d), φ (charX t (Ψ s z), charV t (Ψ s z)) ∂f s) (Set.Icc 0 t)

theorem Vlasov.dualCore_main {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hf_weak : IsVlasovSolutionOn gradW f T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (φ : PhaseSpace d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (Ψ : ℝ → PhaseSpace d → PhaseSpace d) (hΨ_left : ∀ s ∈ Set.Ioo 0 T, Function.LeftInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_right : ∀ s ∈ Set.Ioo 0 T, Function.RightInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) (hΨ_C1 : ContDiffOn ℝ 1 (fun (p : ℝ × PhaseSpace d) => Ψ p.1 p.2) (Set.Ioo 0 T ×ˢ Set.univ)) (hΦt_C1 : ContDiff ℝ 1 fun (z : PhaseSpace d) => (charX t z, charV t z)) (hflowjoint : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)) (hanti : ∀ s ∈ Set.Ioo 0 T, ∀ (z₁ z₂ : PhaseSpace d), dist z₁ z₂ ≤ dist (charX s z₁, charV s z₁) (charX s z₂, charV s z₂) * Real.exp (↑(max 1 L) * s)) : ∫ (z : PhaseSpace d), φ z ∂f t = ∫ (z : PhaseSpace d), φ (charX t z, charV t z) ∂f 0

theorem Vlasov.frozenFlow_inverse_On {d : ℕ} (W : PhysSpace d → ℝ) [AssW2 W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (t : ℝ) => convolveFunctionMeasure gradW (spatialMarginal (f t)) x) (hf_cont_deriv : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂spatialMarginal (f p.1)) (Set.Icc 0 T ×ˢ Set.univ)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : ∃ (Ψ : ℝ → PhaseSpace d → PhaseSpace d), (∀ s ∈ Set.Ioo 0 T, Function.LeftInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) ∧ (∀ s ∈ Set.Ioo 0 T, Function.RightInverse (Ψ s) fun (z : PhaseSpace d) => (charX s z, charV s z)) ∧ ContDiffOn ℝ 1 (fun (p : ℝ × PhaseSpace d) => Ψ p.1 p.2) (Set.Ioo 0 T ×ˢ Set.univ) ∧ (ContDiff ℝ 1 fun (z : PhaseSpace d) => (charX t z, charV t z)) ∧ ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ) ∧ ∀ s ∈ Set.Ioo 0 T, ∀ (z₁ z₂ : PhaseSpace d), dist z₁ z₂ ≤ dist (charX s z₁, charV s z₁) (charX s z₂, charV s z₂) * Real.exp (↑(max 1 L) * s)

theorem Vlasov.dualCore_terminal {d : ℕ} (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (hflowjoint : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)) (φ : PhaseSpace d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hIoo : ∀ t ∈ Set.Ioo 0 T, ∫ (z : PhaseSpace d), φ z ∂f t = ∫ (z : PhaseSpace d), φ (charX t z, charV t z) ∂f 0) : ∫ (z : PhaseSpace d), φ z ∂f T = ∫ (z : PhaseSpace d), φ (charX T z, charV T z) ∂f 0

theorem Vlasov.weak_eq_frozenField_pushforward_dualCore {d : ℕ} (W : PhysSpace d → ℝ) [AssW2 W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf_weak : IsVlasovSolutionOn gradW f T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (t : ℝ) => convolveFunctionMeasure gradW (spatialMarginal (f t)) x) (hf_cont_deriv : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂spatialMarginal (f p.1)) (Set.Icc 0 T ×ˢ Set.univ)) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (hinit : ∀ (z : PhaseSpace d), (charX 0 z, charV 0 z) = z) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (φ : PhaseSpace d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (z : PhaseSpace d), φ z ∂f t = ∫ (z : PhaseSpace d), φ (charX t z, charV t z) ∂f 0

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 the C_c^∞ test class to C¹_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 family G (narrow continuity of the weak solution, consumption form; derivable from the weak eq + moments).
• transportedIntegral_hasDerivAt_zero (#6a) — HasDerivAt I 0 on Ioo 0 t, the diagonal chain rule: ∂_σ via #4 + ∂_r via differentiation-under-the-integral against f 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 (the s → 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 — the t = T endpoint.

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).

theorem Vlasov.weak_eq_frozenField_pushforward_On {d : ℕ} (W : PhysSpace d → ℝ) [AssW2 W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf_weak : IsVlasovSolutionOn gradW f T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (t : ℝ) => convolveFunctionMeasure gradW (spatialMarginal (f t)) x) (hf_cont_deriv : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂spatialMarginal (f p.1)) (Set.Icc 0 T ×ˢ Set.univ)) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (hflow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f t)) charX charV (Set.Ioo 0 T) Set.univ) (hinit : ∀ (z : PhaseSpace d), (charX 0 z, charV 0 z) = z) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (hderivIco : ∀ (z : PhaseSpace d), ∀ s ∈ Set.Ico 0 T, HasDerivWithinAt (fun (s' : ℝ) => (charX s' z, charV s' z)) (vlasovVectorField gradW (fun (t : ℝ) => spatialMarginal (f t)) s (charX s z, charV s z)) (Set.Ici s) s) (t : ℝ) : t ∈ Set.Icc 0 T → f t = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => (charX t z, charV t z)) (f 0)

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.

theorem Vlasov.weak_isLagrangianVlasovSolutionOn {d : ℕ} (W : PhysSpace d → ℝ) [AssW2 W] (gradW : PhysSpace d → PhysSpace d) (hgradW : ∀ (x : PhysSpace d), gradW x = gradient W x) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hT : 0 < T) (hf_weak : IsVlasovSolutionOn gradW f T) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (hf_narrow : ∀ (g : PhaseSpace d → ℝ), Continuous g → HasCompactSupport g → ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), g z ∂f s) (Set.Icc 0 T)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (t : ℝ) => convolveFunctionMeasure gradW (spatialMarginal (f t)) x) (hf_cont_deriv : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂spatialMarginal (f p.1)) (Set.Icc 0 T ×ˢ Set.univ)) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (hTL_PL : LocalSmallnessPLBuffer L T) : IsLagrangianVlasovSolutionOn gradW f T

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).