Generic analysis for the Vlasov variational equation

Picard-series solutions and their parameter dependence, a Grönwall difference-quotient bound, and joint differentiability from continuous partial derivatives. These arguments use only Mathlib, so they can compile independently of the characteristic-flow construction.

noncomputable def Vlasov.picardIter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) : ℕ → ℝ → E

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)

@[simp]

theorem Vlasov.picardIter_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (t : ℝ) : picardIter 𝒜 x₀ 0 t = x₀

theorem Vlasov.picardIter_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (n : ℕ) (t : ℝ) : picardIter 𝒜 x₀ (n + 1) t = ∫ (s : ℝ) in 0..t, (𝒜 s) (picardIter 𝒜 x₀ n s)

theorem Vlasov.picardIter_continuousOn_and_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hcont𝒜 : ContinuousOn 𝒜 (Set.Icc 0 T)) (hbound𝒜 : ∀ t ∈ Set.Icc 0 T, ‖𝒜 t‖ ≤ K) (n : ℕ) : ContinuousOn (picardIter 𝒜 x₀ n) (Set.Icc 0 T) ∧ ∀ t ∈ Set.Icc 0 T, ‖picardIter 𝒜 x₀ n t‖ ≤ (K * t) ^ n / ↑n.factorial * ‖x₀‖

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.

theorem Vlasov.picardSum_continuous_param_joint {Z : Type u_1} {E : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : Z → ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (h𝒜_cont : Continuous fun (p : Z × ℝ) => 𝒜 p.1 p.2) (h𝒜_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖𝒜 z s‖ ≤ K) : ContinuousOn (fun (p : Z × ℝ) => ∑' (n : ℕ), picardIter (𝒜 p.1) x₀ n p.2) (Set.univ ×ˢ Set.Icc 0 T)

Step 3 (i) — joint (z,s) continuity of the Dyson sum (global-hypothesis form). The Picard iterates are jointly continuous, and their common summable majorant gives continuity of the sum on univ ×ˢ Icc 0 T. Fixed-time continuity specializes this result.

theorem Vlasov.picardSum_continuous_param_Icc_joint {Z : Type u_1} {E : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : Z → ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (h𝒜_contOn : ContinuousOn (fun (p : Z × ℝ) => 𝒜 p.1 p.2) (Set.univ ×ˢ Set.Icc 0 T)) (h𝒜_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖𝒜 z s‖ ≤ K) : ContinuousOn (fun (p : Z × ℝ) => ∑' (n : ℕ), picardIter (𝒜 p.1) x₀ n p.2) (Set.univ ×ˢ Set.Icc 0 T)

Step 3 (i) — joint (z,s) continuity of the Dyson sum on a time window. Clamp time into [0,T] so the global form applies, then transfer back by agreement of the iterates on [0,T]. Fixed-time continuity specializes this result.

theorem Vlasov.picardSum_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hcont𝒜 : ContinuousOn 𝒜 (Set.Icc 0 T)) (hbound𝒜 : ∀ t ∈ Set.Icc 0 T, ‖𝒜 t‖ ≤ K) : ContinuousOn (fun (t : ℝ) => ∑' (n : ℕ), picardIter 𝒜 x₀ n t) (Set.Icc 0 T)

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

theorem Vlasov.picardSum_continuous_param {Z : Type u_1} {E : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : Z → ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (h𝒜_cont : Continuous fun (p : Z × ℝ) => 𝒜 p.1 p.2) (h𝒜_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖𝒜 z s‖ ≤ K) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : Continuous fun (z : Z) => ∑' (n : ℕ), picardIter (𝒜 z) x₀ n t

C3 V2-core — the Dyson sum is continuous in a parameter. Restrict joint continuity of the Dyson sum to a fixed time in [0,T]. The uniform majorant and convergence argument live in picardSum_continuous_param_joint, shared by both forms.

theorem Vlasov.picardSum_continuous_param_Icc {Z : Type u_1} {E : Type u_2} [TopologicalSpace Z] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : Z → ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (h𝒜_contOn : ContinuousOn (fun (p : Z × ℝ) => 𝒜 p.1 p.2) (Set.univ ×ˢ Set.Icc 0 T)) (h𝒜_bound : ∀ (z : Z), ∀ s ∈ Set.Icc 0 T, ‖𝒜 z s‖ ≤ K) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : Continuous fun (z : Z) => ∑' (n : ℕ), picardIter (𝒜 z) x₀ n t

Window version of picardSum_continuous_param: restrict the joint window theorem to a fixed time. The clamping and iterate-agreement argument is shared with the joint form.

theorem Vlasov.picardSum_finset_recurrence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hcont𝒜 : ContinuousOn 𝒜 (Set.Icc 0 T)) (hbound𝒜 : ∀ t ∈ Set.Icc 0 T, ‖𝒜 t‖ ≤ K) (N : ℕ) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ∑ n ∈ Finset.range (N + 1), picardIter 𝒜 x₀ n t = x₀ + ∫ (s : ℝ) in 0..t, (𝒜 s) (∑ n ∈ Finset.range N, picardIter 𝒜 x₀ n s)

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.

theorem Vlasov.picardSum_solves_integralEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : ℝ → E →L[ℝ] E) (x₀ : E) (T : ℝ) (hT : 0 ≤ T) (K : ℝ) (hK : 0 ≤ K) (hcont𝒜 : ContinuousOn 𝒜 (Set.Icc 0 T)) (hbound𝒜 : ∀ t ∈ Set.Icc 0 T, ‖𝒜 t‖ ≤ K) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ∑' (n : ℕ), picardIter 𝒜 x₀ n t = x₀ + ∫ (s : ℝ) in 0..t, (𝒜 s) (∑' (n : ℕ), picardIter 𝒜 x₀ n s)

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

theorem Vlasov.exists_linearODE_solution_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (𝒜 : ℝ → E →L[ℝ] E) (T : ℝ) (hT : 0 ≤ T) (h𝒜 : ContinuousOn 𝒜 (Set.Icc 0 T)) (x₀ : E) : ∃ (M : ℝ → E), M 0 = x₀ ∧ ContinuousOn M (Set.Icc 0 T) ∧ ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt M ((𝒜 t) (M t)) (Set.Icc 0 T) t

Existence for a linear ODE with continuous coefficients on a compact interval. The Picard sum gives an explicit solution. Its summable factorial majorant supplies continuity, and its integral equation supplies the derivative through the fundamental theorem of calculus.

theorem Vlasov.exists_fundamentalMatrix {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)) : ∃ (M : ℝ → F →L[ℝ] F), M 0 = ContinuousLinearMap.id ℝ F ∧ ContinuousOn M (Set.Icc 0 T) ∧ ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt M (A t ∘SL M t) (Set.Icc 0 T) t

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

theorem Vlasov.continuousOn_prod_of_lipschitz_continuousOn {Z : Type u_1} {E : Type u_2} [PseudoMetricSpace Z] [PseudoMetricSpace E] (G : Z → ℝ → E) (T C : ℝ) (hlip : ∀ s ∈ Set.Icc 0 T, ∀ (z₁ z₂ : Z), dist (G z₁ s) (G z₂ s) ≤ C * dist z₁ z₂) (hcont : ∀ (z : Z), ContinuousOn (fun (s : ℝ) => G z s) (Set.Icc 0 T)) : ContinuousOn (fun (p : Z × ℝ) => G p.1 p.2) (Set.univ ×ˢ Set.Icc 0 T)

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.

theorem Vlasov.gronwall_diffQuotient_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (vlin : ℝ → E →L[ℝ] E) (K : NNReal) (hvlin_lip : ∀ (s : ℝ), LipschitzWith K ⇑(vlin s)) (uh mh Fuh : ℝ → E) (εf T t : ℝ) (ht : t ∈ Set.Ioo 0 T) (huh_cont : ContinuousOn uh (Set.Icc 0 T)) (hmh_cont : ContinuousOn mh (Set.Icc 0 T)) (huh_deriv : ∀ s ∈ Set.Ioo 0 T, HasDerivAt uh (Fuh s) s) (hmh_deriv : ∀ s ∈ Set.Ioo 0 T, HasDerivAt mh ((vlin s) (mh s)) s) (hdefect : ∀ s ∈ Set.Ioo 0 T, dist (Fuh s) ((vlin s) (uh s)) ≤ εf) (h0 : uh 0 = mh 0) : dist (uh t) (mh t) ≤ gronwallBound 0 (↑K) εf t

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

theorem Vlasov.hasFDerivAt_of_continuous_partials {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f Ds : ℝ × E → F} {Dz₀ : E →L[ℝ] F} (s₀ : ℝ) (z₀ : E) (hDs : ∀ (p : ℝ × E), HasDerivAt (fun (s : ℝ) => f (s, p.2)) (Ds p) p.1) (hDs_cont : Continuous Ds) (hDz₀ : HasFDerivAt (fun (z : E) => f (s₀, z)) Dz₀ z₀) : HasFDerivAt f ((ContinuousLinearMap.fst ℝ ℝ E).smulRight (Ds (s₀, z₀)) + Dz₀ ∘SL ContinuousLinearMap.snd ℝ ℝ E) (s₀, z₀)

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

theorem Vlasov.hasFDerivAt_of_continuous_partials_open {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f Ds : ℝ × E → F} {Dz₀ : E →L[ℝ] F} {U : Set (ℝ × E)} (hU : IsOpen U) {s₀ : ℝ} {z₀ : E} (hmem : (s₀, z₀) ∈ U) (hDs : ∀ p ∈ U, HasDerivAt (fun (s : ℝ) => f (s, p.2)) (Ds p) p.1) (hDs_cont : ContinuousOn Ds U) (hDz₀ : HasFDerivAt (fun (z : E) => f (s₀, z)) Dz₀ z₀) : HasFDerivAt f ((ContinuousLinearMap.fst ℝ ℝ E).smulRight (Ds (s₀, z₀)) + Dz₀ ∘SL ContinuousLinearMap.snd ℝ ℝ E) (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).