Local well-posedness for the Vlasov equation

The Picard fixed point supplies the local characteristic flow, its moment bound, and the local Lagrangian solution. Continuation and stability use these results without retaining their elaboration in the same compilation unit.

§9 Theorem (Existence and uniqueness for Vlasov) (tex: thm:vlasov-wp)

theorem Vlasov.integrable_gradW_shift {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (μ : MeasureTheory.Measure (PhysSpace d)) [MeasureTheory.IsFiniteMeasure μ] (h_yint : MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) μ) (xp : PhysSpace d) : MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (xp - y)) μ

Lipschitz growth of the force plus a first moment of the measure make the shifted force integrable. The workhorse integrability fact behind every convolveFunctionMeasure estimate.

theorem Vlasov.LocalSmallnessContraction.gronwallBound_lt_one {L : NNReal} {T : ℝ} (hTL_con : LocalSmallnessContraction L T) : gronwallBound 0 (↑(max 1 L)) (↑L) T < 1

LocalSmallnessContraction L T IS the Grönwall contraction factor gronwallBound 0 (max 1 L) L T < 1, after unfolding both definitions.

theorem Vlasov.vlasovWellPosedness_local_picard_fixedPointFlow {d : ℕ} [NeZero d] (W : PhysSpace d → ℝ) (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)) [MeasureTheory.IsProbabilityMeasure f₀] (hf₀_int : MeasureTheory.Integrable (fun (z : PhaseSpace d) => ‖z‖) f₀) {T : ℝ} (hT : 0 < T) (hTL_PL : LocalSmallnessPLBuffer L T) (hTL_con : LocalSmallnessContraction L T) (hB : ↑L / (1 + ↑L) * (Real.exp ((1 + ↑L) * T) - 1) < 1) : ∃ (charX : ℝ → PhaseSpace d → PhysSpace d) (charV : ℝ → PhaseSpace d → PhysSpace d) (M_ρ : ℝ), 0 ≤ M_ρ ∧ IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) charX charV (Set.Ioo 0 T) Set.univ ∧ (∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fun (s : ℝ) => charX s z) (charV t z) (Set.Icc 0 T) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV s z) (-convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) (charX t z)) (Set.Icc 0 T) t) ∧ (∀ s ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s) ≤ M_ρ) ∧ (∀ s ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))) ∧ (∀ (s : ℝ), Continuous fun (x : PhysSpace d) => convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s)) x) ∧ (∀ (s : ℝ), AEMeasurable (fun (z : PhaseSpace d) => (charX s z, charV s z)) f₀) ∧ ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))

Sub-helper for vlasovWellPosedness_local — the Picard fixed-point self-consistent flow.

Given f₀ : Measure (PhaseSpace d) with finite first moment, produces a characteristic flow (charX, charV) whose own pushforward's spatial marginal is the reference measure the flow is built against — i.e., the Picard fixed point at the spatial-marginal-curve level:

ρ_t := spatialMarginal (Measure.map (z ↦ (charX t z, charV t z)) f₀) charX, charV solve the Vlasov ODE against this ρ.

The body carries the substantive Picard analysis:

• M-fixed-point: pick a moment bound M ≥ A/(1 - B) where A = gronwallBound 1 (1+L) ‖gradW 0‖ T · (M_f₀ + 1) and B = L · (exp((1+L)·T) - 1)/(1+L) · (M_f₀ + 1). Requires B < 1, which is the genuine convergence criterion for the moment iteration (stronger than the contraction predicate LocalSmallnessContraction L T alone for large M_f₀ — the contraction predicate gates the q factor; the M-fixed-point additionally requires the moment iteration to converge).
• Picard sequence x_n : ℕ → VlasovMeasureCurve d T M starting from x_0 := constantCurve (spatialMarginal f₀) and x_{n+1} := Phi_step(x_n).
• Contraction via Phi_supW1_contraction: supW1On (Φρ) (Φσ) ≤ q · D with q < 1. Apply picard_iterate_isCauchy_of_contraction + picard_iterate_exists_limit to get the W₁-limit ρ_lim : VlasovMeasureCurve d T M.
• Self-consistency Φ(ρ_lim) = ρ_lim: triangle through x_n.
• Apply exists_vlasov_characteristicFlow_global_smallT to ρ_lim.extend to get the flow.

Metric-dependence note. The convergence rests on two independent predicates:

• LocalSmallnessContraction L T := L · (exp((max 1 L)·T) - 1) / (max 1 L) < 1 — exponential in T, from Phi_supW1_contraction's W₁-based shape.
• LocalSmallnessPLBuffer L T := L · T² < 1 — quadratic, from per-ball Picard-Lindelöf's ball geometry.

These are genuinely independent (neither universally implies the other), so each predicate matches its own sub-argument.

Under the Wbar refactor (Dobrushin 1979, §5), both constraints become linear-in-T and align: LocalSmallnessContraction reduces to C₂(L)·T < 1, and the single algebraic constraint then suffices and is satisfiable for any L > 0 by taking T < 1/C₂(L).

Output bundle (designed to feed vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn directly):

• Flow (charX, charV) against the spatial marginal of the pushforward — the load-bearing self-consistency conjunct.
• Boundary regularity.
• Uniform moment bound M_ρ on the spatial marginal trajectory.

theorem Vlasov.vlasovWellPosedness_local_moment {d : ℕ} (W : PhysSpace d → ℝ) (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)) [MeasureTheory.IsProbabilityMeasure f₀] (hf₀_int : MeasureTheory.Integrable (fun (z : PhaseSpace d) => ‖z‖) f₀) {T : ℝ} (hT : 0 < T) (_hTL_PL : LocalSmallnessPLBuffer L T) (_hTL_con : LocalSmallnessContraction L T) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hflow_on : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) charX charV (Set.Ioo 0 T) Set.univ) (h_boundary : ∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fun (s : ℝ) => charX s z) (charV t z) (Set.Icc 0 T) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV s z) (-convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) (charX t z)) (Set.Icc 0 T) t) (hM_ρ_bound : ∀ s ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s) ≤ M_ρ) (h_y_int_ρ : ∀ s ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))) (_hconv_cont : ∀ (s : ℝ), Continuous fun (x : PhysSpace d) => convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s)) x) (h_aemeas : ∀ (s : ℝ), AEMeasurable (fun (z : PhaseSpace d) => (charX s z, charV s z)) f₀) (h_int_conv : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : HasFiniteFirstMoment (vlasovSolutionViaPushforward charX charV f₀ t)

Sub-helper for vlasovWellPosedness_local — moment-bound transport.

Given the Picard fixed-point flow's bundle (from _picard_fixedPointFlow), produces HasFiniteFirstMoment (f t) for t ∈ Icc 0 T, where f := vlasovSolutionViaPushforward charX charV f₀.

Proof strategy:

1. Boundary transport: extract h_init / h_cont_Icc / h_deriv_Ico from hflow_on + h_boundary via characteristicFlow_boundary_regularity.
2. flow_distance_growth_bound_on applied to (charX, charV) produces the growth constant C_T with ‖(charX t z, charV t z)‖ ≤ C_T * (‖z‖ + 1).
3. Probability of f t = Measure.map (z ↦ (charX t z, charV t z)) f₀ from the AEMeasurable witness.
4. Integrable ‖·‖ on f t: via integrable_map_measure + growth bound + Integrable ‖·‖ f₀.

Factored out to keep vlasovWellPosedness_local's body a clean glue.

theorem Vlasov.vlasovWellPosedness_local_isLagrangian {d : ℕ} (W : PhysSpace d → ℝ) (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)) [MeasureTheory.IsProbabilityMeasure f₀] (hf₀_int : MeasureTheory.Integrable (fun (z : PhaseSpace d) => ‖z‖) f₀) {T : ℝ} (hT : 0 < T) (_hTL_PL : LocalSmallnessPLBuffer L T) (_hTL_con : LocalSmallnessContraction L T) (charX charV : ℝ → PhaseSpace d → PhysSpace d) (M_ρ : ℝ) (hM_ρ_nn : 0 ≤ M_ρ) (hflow_on : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) charX charV (Set.Ioo 0 T) Set.univ) (h_boundary : ∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fun (s : ℝ) => charX s z) (charV t z) (Set.Icc 0 T) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV s z) (-convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ t)) (charX t z)) (Set.Icc 0 T) t) (hM_ρ_bound : ∀ s ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s) ≤ M_ρ) (h_y_int_ρ : ∀ s ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))) (hconv_cont : ∀ (s : ℝ), Continuous fun (x : PhysSpace d) => convolveFunctionMeasure gradW (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s)) x) (h_aemeas : ∀ (s : ℝ), AEMeasurable (fun (z : PhaseSpace d) => (charX s z, charV s z)) f₀) (h_int_conv : ∀ (s : ℝ) (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (spatialMarginal (vlasovSolutionViaPushforward charX charV f₀ s))) : IsLagrangianVlasovSolutionOn gradW (vlasovSolutionViaPushforward charX charV f₀) T

Sub-helper for vlasovWellPosedness_local — IsLagrangianVlasovSolutionOn threading.

Given the Picard fixed-point flow's bundle (from _picard_fixedPointFlow), produces the IsLagrangianVlasovSolutionOn gradW f T conjunct via the 20-hypothesis threading through vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn.

Proof strategy:

1. Boundary transport: extract h_init / h_cont_Icc / h_deriv_Ico.
2. Universal-in-s convolution integrability (handling s outside [0, T] via the clamp-extension argument).
3. AEMeasurable witness.
4. IsCharacteristicFlowSelfConsistent: ∀ t, ρ_lim t = Φ charX f₀ t, which expands by definition since ρ_lim = spatialMarginal ∘ f and f = vlasovSolutionViaPushforward charX charV f₀; spatial marginal of pushforward = pushforward under Prod.fst ∘ ... = Φ charX f₀. The composition is the Measure.map_map-with-AEMeasurable bridge.
5. Continuity of gradW: hL.continuous.
6. Probability instance of spatialMarginal ∘ f: derived from AEMeasurable + IsProbabilityMeasure f₀.
7. Final invocation: vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn with the full hypothesis bundle.

Factored out to keep vlasovWellPosedness_local's body a clean glue.

theorem Vlasov.vlasovWellPosedness_local {d : ℕ} [NeZero d] (W : PhysSpace d → ℝ) (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)) (hf₀ : HasFiniteFirstMoment f₀) {T : ℝ} (hT : 0 < T) (hTL_PL : LocalSmallnessPLBuffer L T) (hTL_con : LocalSmallnessContraction L T) (hB : ↑L / (1 + ↑L) * (Real.exp ((1 + ↑L) * T) - 1) < 1) : ∃ (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (charX : ℝ → PhaseSpace d → PhysSpace d) (charV : ℝ → PhaseSpace d → PhysSpace d), f 0 = f₀ ∧ (∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) ∧ (∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M) ∧ IsLagrangianVlasovSolutionOn gradW f T ∧ (∀ t ∈ Set.Icc 0 T, f t = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => (charX t z, charV t z)) (f 0)) ∧ (∀ s ∈ Set.Icc 0 T, AEMeasurable (fun (z : PhaseSpace d) => (charX s z, charV s z)) (f 0)) ∧ (∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fun (s : ℝ) => charX s z) (charV t z) (Set.Icc 0 T) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV s z) (-convolveFunctionMeasure gradW (spatialMarginal (f t)) (charX t z)) (Set.Icc 0 T) t) ∧ ∀ (z : PhaseSpace d), charX 0 z = z.1 ∧ charV 0 z = z.2

Local existence of a Vlasov solution on [0, T].

Under the joint constraint LocalSmallnessPLBuffer L T (L · T² < 1) + LocalSmallnessContraction L T, produces a local-time Vlasov solution f : ℝ → Measure (PhaseSpace d) on [0, T] satisfying initial condition + local finite first moment + IsLagrangianVlasovSolutionOn.

The forward-iteration continuation extends from local T to arbitrary T_target via fixed-T_0 iteration: the contraction time T_0 depends only on L (not on the moment bound M_n propagating through iterations), because Phi_supW1_contraction's q is gronwallBound 0 (max 1 L) (L · D) T — independent of M_n. So the continuation iterates [0, T_0], [T_0, 2 T_0], … with constant step T_0, reaching any T_target in ⌈T_target / T_0⌉ windows; gluing then bridges from IsLagrangianVlasovSolutionOn (local) to IsLagrangianVlasovSolution (global).

Proof strategy:

1. Initial spatial marginal: μ₀ := spatialMarginal f₀. By HasFiniteFirstMoment f₀, μ₀ is a probability measure with Integrable ‖·‖. Let M_f₀ := ∫ ‖z‖ ∂f₀ (finite by hf₀.2.integral_norm_le).

2. Picard sequence on spatial marginals:

   • ρ_0 := constantCurve μ₀.
   • ρ_{n+1} obtained via Phi_step applied to ρ_n's flow.

   Each ρ_n lives in VlasovMeasureCurve d T M for an appropriate M chosen so that the growth bound from flow_distance_growth_bound_on stays within M across iterations (the M-preservation constraint).

3. Contraction estimate via Phi_supW1_contraction: supW1On (ρ_n.ρ) (ρ_{n+1}.ρ) ≤ ENNReal.ofReal (q^n * D₀) for q := gronwallBound 0 (max 1 L) (L · D) T < 1 (since T is small enough per the joint constraint).

4. Apply picard_iterate_isCauchy_of_contraction to get the ENNReal-form Cauchy condition on the supW1On pseudodistance.

5. Apply picard_iterate_exists_limit to extract the limit ρ_lim : VlasovMeasureCurve d T M plus pointwise W₁-tendsto.

6. Self-consistency Φ(ρ_lim) = ρ_lim: triangle through ρ_n using the uniform-tendsto helper, contraction, and pointwise tendsto.

7. Apply exists_vlasov_characteristicFlow_global_smallT to ρ_lim.extend to get the characteristic flow (charX, charV) against the self-consistent limit.

8. Define f := vlasovSolutionViaPushforward charX charV f₀. Verify:

   • f 0 = f₀ (from IsCharacteristicFlowOn's initial-condition clause + Measure.map_id).
   • HasFiniteFirstMoment (f t) on [0, T] (from flow_distance_growth_bound_on applied to (charX, charV) + hf₀.2).
   • IsLagrangianVlasovSolutionOn gradW f T via vlasovSolutionViaPushforward_isLagrangianVlasovSolutionOn.

The body invokes vlasovWellPosedness_local_picard_fixedPointFlow for the Picard fixed-point flow, then vlasovWellPosedness_local_finalAssembly_* for the moment and Lagrangian conjuncts, deriving f 0 = f₀ inline.