Differentiability and inversion of the frozen Vlasov flow

The variational equation gives the spatial and joint derivatives of the flow and its inverse. The Jacobian and explicit fundamental matrix remain together so their generated proof declarations are shared as before.

noncomputable def Vlasov.vlasovFieldJacobian {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) (p : ℝ × PhaseSpace d) : PhaseSpace d →L[ℝ] PhaseSpace d

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.

theorem Vlasov.vlasovFieldJacobian_continuousOn {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) (T : ℝ) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × PhaseSpace d) => vlasovFieldJacobian gradW ρ p) (Set.Icc 0 T ×ˢ Set.univ)

Joint continuity of the Jacobian on Icc 0 T ×ˢ univ. Express the block map as a sum of continuous compositions of the convolution derivative.

theorem Vlasov.vlasovField_taylorRemainder_uniform {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (z : PhaseSpace d) (hcontIcc : ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (η : ℝ) : 0 < η → ∃ (δ : ℝ), 0 < δ ∧ ∀ s ∈ Set.Icc 0 T, ∀ (w : PhaseSpace d), ‖w - (charX s z, charV s z)‖ ≤ δ → ‖vlasovVectorField gradW ρ s w - vlasovVectorField gradW ρ s (charX s z, charV s z) - (vlasovFieldJacobian gradW ρ (s, charX s z, charV s z)) (w - (charX s z, charV s z))‖ ≤ η * ‖w - (charX s z, charV s z)‖

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.

noncomputable def Vlasov.fundamentalMatrix {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (A : ℝ → F →L[ℝ] F) : ℝ → F →L[ℝ] F

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

theorem Vlasov.fundamentalMatrix_spec {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : ℝ → F →L[ℝ] F) (T : ℝ) (hT : 0 ≤ T) (hA : ContinuousOn A (Set.Icc 0 T)) : fundamentalMatrix A 0 = ContinuousLinearMap.id ℝ F ∧ ContinuousOn (fundamentalMatrix A) (Set.Icc 0 T) ∧ ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fundamentalMatrix A) (A t ∘SL fundamentalMatrix A t) (Set.Icc 0 T) t

fundamentalMatrix A solves the fundamental-matrix IVP on [0,T] (the non-existential form of exists_fundamentalMatrix; same proof through the picardSum lemmas).

theorem Vlasov.fundamentalMatrix_continuous_param {Z : Type u_1} {F : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : Z → ℝ → F →L[ℝ] F) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hA_contOn : ContinuousOn (fun (p : Z × ℝ) => A p.1 p.2) (Set.univ ×ˢ Set.Icc 0 T)) (hA_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖A z s‖ ≤ K) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : Continuous fun (z : Z) => fundamentalMatrix (A z) t

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.

theorem Vlasov.fundamentalMatrix_continuous_param_joint {Z : Type u_1} {F : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : Z → ℝ → F →L[ℝ] F) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hA_contOn : ContinuousOn (fun (p : Z × ℝ) => A p.1 p.2) (Set.univ ×ˢ Set.Icc 0 T)) (hA_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖A z s‖ ≤ K) : ContinuousOn (fun (p : Z × ℝ) => fundamentalMatrix (A p.1) p.2) (Set.univ ×ˢ Set.Icc 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)).

theorem Vlasov.charFlow_hasFDerivAt_of_fundamentalMatrix {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (z : PhaseSpace d) (hcontIcc : ∀ (z' : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z', charV s z')) (Set.Icc 0 T)) (Mz : ℝ → PhaseSpace d →L[ℝ] PhaseSpace d) (hMz0 : Mz 0 = ContinuousLinearMap.id ℝ (PhaseSpace d)) (hMzcont : ContinuousOn Mz (Set.Icc 0 T)) (hMzderiv : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt Mz (vlasovFieldJacobian gradW ρ (s, charX s z, charV s z) ∘SL Mz s) (Set.Icc 0 T) s) (t : ℝ) : t ∈ Set.Ioo 0 T → HasFDerivAt (fun (w : PhaseSpace d) => (charX t w, charV t w)) (Mz t) z

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_h is exact — its defect is 0 (its derivative (A·Mz)(s)·h = A(s)·m_h(s) by hMzderiv + HasDerivWithinAt.clm_apply).
• u_h's defect is the Taylor remainder R(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 in s. The frozen field's two-sided ODE holds only on Ioo 0 T, so apply dist_le_of_approx_trajectories_ODE on [s₀, t] (s₀ ∈ Ioo 0 t) and take s₀ → 0⁺ (the initial defect dist(u_h s₀, m_h s₀) → 0 by continuity), giving ‖u_h t − m_h t‖ ≤ gronwallBound 0 K εf t = εf·(exp(K t)−1)/K. Since η is arbitrary this is o(‖h‖). K := max 1 L is the uniform field Lipschitz constant; ‖A(s,·)‖ ≤ K via norm_fderiv_le_of_lipschitz. (hcontIcc is universal in the initial point because the s₀→0⁺ limit needs continuity of Φ_·(z+h), M2.)

theorem Vlasov.charFlow_hasFDerivAt_in_initialPoint {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) : ∃ (Dflow : ℝ → PhaseSpace d → PhaseSpace d →L[ℝ] PhaseSpace d), (∀ t ∈ Set.Ioo 0 T, ∀ (z : PhaseSpace d), HasFDerivAt (fun (w : PhaseSpace d) => (charX t w, charV t w)) (Dflow t z) z) ∧ ∀ t ∈ Set.Ioo 0 T, Continuous (Dflow t)

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 in x (that needs W ∈ C³; AssW2 gives only C²), 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.

theorem Vlasov.charFlow_antilipschitzInZ_via_gronwall_Ioo {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (t : ℝ), MeasureTheory.IsProbabilityMeasure (ρ t)] (h_int : ∀ (t : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ t)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (h_init : ∀ (z : PhaseSpace d), (charX 0 z, charV 0 z) = z) (h_cont_Icc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (h_deriv2 : ∀ (z : PhaseSpace d), ∀ s ∈ Set.Ioo 0 T, HasDerivAt (fun (s' : ℝ) => (charX s' z, charV s' z)) (vlasovVectorField gradW ρ s (charX s z, charV s z)) s) (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ (z₁ z₂ : PhaseSpace d), dist z₁ z₂ ≤ dist (charX t z₁, charV t z₁) (charX t z₂, charV t z₂) * Real.exp (↑(max 1 L) * (t - 0))

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.

theorem Vlasov.antilipschitzWith_fderiv_of_antilipschitz {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ] F} {x : E} {C : NNReal} (hf : AntilipschitzWith C f) (hf' : HasFDerivAt f f' x) : AntilipschitzWith C ⇑f'

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

theorem Vlasov.exists_global_c1_inverse_of_antilipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Φ : E → E} {M : E → E →L[ℝ] E} {Ca Cl : NNReal} (hderiv : ∀ (z : E), HasFDerivAt Φ (M z) z) (hM_cont : Continuous M) (hanti : AntilipschitzWith Ca Φ) (hlip : LipschitzWith Cl Φ) : ∃ (Ψ : E → E) (e : E → E ≃L[ℝ] E), (∀ (z : E), ↑(e z) = M z) ∧ Function.LeftInverse Ψ Φ ∧ Function.RightInverse Ψ Φ ∧ LipschitzWith Ca Ψ ∧ ∀ (w : E), HasFDerivAt Ψ (↑(e (Ψ w)).symm) w

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.

theorem Vlasov.exists_charFlow_inverse_On {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Ioo 0 T → ∃ (Ψ : PhaseSpace d → PhaseSpace d) (e : PhaseSpace d → PhaseSpace d ≃L[ℝ] PhaseSpace d), (∀ (z : PhaseSpace d), HasFDerivAt (fun (w : PhaseSpace d) => (charX t w, charV t w)) (↑(e z)) z) ∧ (Function.LeftInverse Ψ fun (z : PhaseSpace d) => (charX t z, charV t z)) ∧ (Function.RightInverse Ψ fun (z : PhaseSpace d) => (charX t z, charV t z)) ∧ Continuous Ψ ∧ ∀ (w : PhaseSpace d), HasFDerivAt Ψ (↑(e (Ψ w)).symm) w

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.

theorem Vlasov.charFlow_continuousOn_joint {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 ≤ T) (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)) (hderiv : ∀ (z : PhaseSpace d), ∀ s ∈ Set.Ioo 0 T, HasDerivWithinAt (fun (s : ℝ) => (charX s z, charV s z)) (vlasovVectorField gradW ρ s (charX s z, charV s z)) (Set.Ici s) s) : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)

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.

theorem Vlasov.vlasovField_along_flow_continuousOn {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (s : ℝ) => convolveFunctionMeasure gradW (ρ s) x) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hflowjoint : ContinuousOn (fun (p : ℝ × PhaseSpace d) => (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × PhaseSpace d) => vlasovVectorField gradW ρ p.1 (charX p.1 p.2, charV p.1 p.2)) (Set.Icc 0 T ×ˢ Set.univ)

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

theorem Vlasov.charFlow_hasFDerivAt_joint {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (s : ℝ) => convolveFunctionMeasure gradW (ρ s) x) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) : ∃ (DΦ : ℝ × PhaseSpace d → ℝ × PhaseSpace d →L[ℝ] PhaseSpace d), (∀ p ∈ Set.Ioo 0 T ×ˢ Set.univ, HasFDerivAt (fun (q : ℝ × PhaseSpace d) => (charX q.1 q.2, charV q.1 q.2)) (DΦ p) p) ∧ ContinuousOn DΦ (Set.Ioo 0 T ×ˢ Set.univ)

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.

theorem Vlasov.charFlow_contDiffAt_joint {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (s : ℝ) => convolveFunctionMeasure gradW (ρ s) x) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 0 T)) (p : ℝ × PhaseSpace d) : p ∈ Set.Ioo 0 T ×ˢ Set.univ → ContDiffAt ℝ 1 (fun (q : ℝ × PhaseSpace d) => (charX q.1 q.2, charV q.1 q.2)) p

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.

theorem Vlasov.charFlow_inverse_contDiffOn_joint {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (hgradW_C1 : ContDiff ℝ 1 gradW) (L : NNReal) (hL : LipschitzWith L gradW) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) [∀ (s : ℝ), MeasureTheory.IsProbabilityMeasure (ρ s)] (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T : ℝ) (hT : 0 < T) (hflow : IsCharacteristicFlowOn gradW ρ charX charV (Set.Ioo 0 T) Set.univ) (h_int : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (ρ s)) (hf_cont : ∀ (x : PhysSpace d), Continuous fun (s : ℝ) => convolveFunctionMeasure gradW (ρ s) x) (hρD_cont : ContinuousOn (fun (p : ℝ × PhysSpace d) => ∫ (y : PhysSpace d), fderiv ℝ gradW (p.2 - y) ∂ρ p.1) (Set.Icc 0 T ×ˢ Set.univ)) (hcontIcc : ∀ (z : PhaseSpace d), ContinuousOn (fun (s : ℝ) => (charX s z, charV s z)) (Set.Icc 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)

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

1. Forward chart Ξ : (s,z) ↦ (s, Φ_s z) is ContDiffAt ℝ 1 at each (s₀,z₀) ∈ Ioo 0 T ×ˢ univ. Φ := (charX·, charV·) is jointly C¹ (charFlow_hasFDerivAt_joint, item (iii) — ∃ DΦ, HasFDerivAt-everywhere + ContinuousOn DΦ); lift to ContDiffAt ℝ 1 Φ via contDiffAt_succ_iff_hasFDerivAt (Mathlib/.../ContDiff/Defs.lean:994, n := 0: feed DΦ, the open nbhd U ∈ 𝓝, HasFDerivAt-on-U, and ContDiffAt 0 DΦ from contDiffAt_zero + ContinuousOn DΦ U). Ξ = (fst, Φ) so ContDiffAt ℝ 1 Ξ via ContDiffAt.prod with contDiffAt_fst.
2. DΞ(s₀,z₀) is an invertible ≃L. Block-lower-triangular (h,k) ↦ (h, h•b + M·k) with b := b_{s₀}(Φ_{s₀}z₀), M := M_{s₀}z₀ invertible (Step 2's e₀ z₀). Build the ℝ×E ≃L ℝ×E via ContinuousLinearEquiv.ofBijective (inject: (h,k)↦0 ⇒ h=0, then M k=0 ⇒ k=0; finite-dim LinearMap.injective_iff_surjective). HasStrictFDerivAt Ξ (this ≃L) (s₀,z₀) via ContDiffAt.hasStrictFDerivAt'.
3. Local C¹ inverse + patch. ContDiffAt.to_localInverse (Mathlib/.../InverseFunctionTheorem/ContDiff.lean:66) ⇒ Ξ.localInverse is ContDiffAt ℝ 1 at Ξ(s₀,z₀) = (s₀, Φ_{s₀}z₀). The global (s,w)↦(s, Ψ_s w) agrees with Ξ.localInverse on a nbhd (both left-inverses; Ξ injective on Ioo 0 T ×ˢ univ since s is preserved + each Φ_s injective per Step 2) ⇒ ContDiffAt.congr ⇒ (s,w)↦(s,Ψ_s w) is ContDiffAt ℝ 1 at each point ⇒ ContDiffOn ℝ 1 (projecting off the s component, ContDiffAt.snd).
4. Bijectivity is the per-slice LeftInverse/RightInverse from exists_charFlow_inverse_On, packaged into the s-indexed Ψ. The two-time flow Φ_{s→t} = Φ_t ∘ Ψ_s is then jointly C¹ 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:

theorem Vlasov.twoTimeFlow_contDiffOn_joint {d : ℕ} (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T t : ℝ) (Ψ : ℝ → PhaseSpace d → PhaseSpace d) (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)) : ContDiffOn ℝ 1 (fun (p : ℝ × PhaseSpace d) => (charX t (Ψ p.1 p.2), charV t (Ψ p.1 p.2))) (Set.Ioo 0 T ×ˢ Set.univ)

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.

theorem Vlasov.transportedTest_transport_identity {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (ρ : ℝ → MeasureTheory.Measure (PhysSpace d)) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (T t : ℝ) (φ : PhaseSpace d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (Ψ : ℝ → 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)) (hflow_ode : ∀ (z : PhaseSpace d), ∀ s ∈ Set.Ioo 0 T, HasDerivAt (fun (s' : ℝ) => (charX s' z, charV s' z)) (vlasovVectorField gradW ρ s (charX s z, charV s z)) s) (s : ℝ) (hs : s ∈ Set.Ioo 0 T) (w : PhaseSpace d) : HasDerivAt (fun (s' : ℝ) => φ (charX t (Ψ s' w), charV t (Ψ s' w))) (-(fderiv ℝ (fun (w' : PhaseSpace d) => φ (charX t (Ψ s w'), charV t (Ψ s w'))) w) (vlasovVectorField gradW ρ s w)) s

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 jointly C¹ on Ioo 0 T ×ˢ univ (4a + φ smooth), so HasFDerivAt (uncurry ψ) Dψ (s,w) at the interior point (s,w), with Dψ the joint Fréchet derivative.
• Constancy curve: set z₀ := Ψ_s w, so w = Φ_s z₀ (hΨ_right). The composite s' ↦ ψ_{s'}(Φ_{s'} z₀) = φ(Φ_t(Ψ_{s'}(Φ_{s'} z₀))) = φ(Φ_t z₀) is constant in s' (hΨ_left: Ψ_{s'} ∘ Φ_{s'} = id), hence has zero s'-derivative.
• The curve c(s') := (s', Φ_{s'} z₀) has HasDerivAt c (1, b_s w) s (hflow_ode + id), with c(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) (compose uncurry ψ with s' ↦ (s', w)) and Dψ(s,w)(0,k) = (fderiv ℝ (ψ s) w) k (compose with w' ↦ (s, w')). Surjectivity (hΨ_right) covers every w. Rearrange to the claimed HasDerivAt.