Continuation of local Vlasov solutions

Boundary gluing and iteration extend a local Lagrangian solution to any finite horizon. Stability and the global theorem use this continuation independently.

Banked infrastructure: localized hasDerivAt_of_hasDerivAt_of_ne

theorem Vlasov.hasDerivAt_of_hasDerivAt_of_ne_in_nhds {f g : ℝ → ℝ} {x₀ : ℝ} (h_diff_ne : ∀ᶠ (y : ℝ) in nhds x₀, y ≠ x₀ → HasDerivAt f (g y) y) (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) : HasDerivAt f (g x₀) x₀

Local version of hasDerivAt_of_hasDerivAt_of_ne (Mathlib/Analysis/Calculus/ FDeriv/Extend.lean): if f : ℝ → ℝ has HasDerivAt with derivative g(y) at every y ≠ x₀ in some neighborhood of x₀, and both f and g are continuous at x₀, then f has HasDerivAt with derivative g(x₀) at x₀.

The proof composes hasDerivWithinAt_Iic_of_tendsto_deriv (left side) + hasDerivWithinAt_Ici_of_tendsto_deriv (right side) + HasDerivWithinAt.union, following the Mathlib lemma's proof structure but with locally-quantified hypothesis (enabling use when the punctured-HasDerivAt holds only on a bounded interval, not all of ℝ).

Variable-T_target continuation via fixed-T_0 iteration

theorem Vlasov.flowConv_continuousWithinAt_Iic_seam {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (charX : ℝ → PhaseSpace d → PhysSpace d) (f₀ : MeasureTheory.Measure (PhaseSpace d)) [MeasureTheory.IsProbabilityMeasure f₀] (hf₀_int : MeasureTheory.Integrable (fun (z : PhaseSpace d) => ‖z‖) f₀) {T : ℝ} (hT : 0 < T) (μ : ℝ → MeasureTheory.Measure (PhysSpace d)) (h_push : ∀ s ∈ Set.Icc 0 T, μ s = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => charX s z) f₀) (h_aemeas : ∀ s ∈ Set.Icc 0 T, AEMeasurable (fun (z : PhaseSpace d) => charX s z) f₀) (h_charX_cont : ∀ (z : PhaseSpace d), ContinuousWithinAt (fun (s : ℝ) => charX s z) (Set.Icc 0 T) T) (C_T : ℝ) (_hC_T_nn : 0 ≤ C_T) (hC_T : ∀ s ∈ Set.Icc 0 T, ∀ (z : PhaseSpace d), ‖charX s z‖ ≤ C_T * (‖z‖ + 1)) (z : PhaseSpace d) : ContinuousWithinAt (fun (s : ℝ) => convolveFunctionMeasure gradW (μ s) (charX s z)) (Set.Iic T) T

Route 2 inner kernel for glue_step h_cont_g (LEFT / Iic T): continuity at the seam T of s ↦ (∇W ∗ μ_s)(charX s z), where the window measure curve μ is the flow-pushforward of f₀.

Proven from PROVEN tools only (no deferred OT). The pushforward rewrite (∇W ∗ μ_s)(x) = ∫ z', gradW (x − charX s z') ∂f₀ (integral_map) turns the moving-measure convolution into a fixed-f₀ integral with moving integrand, closed by dominated convergence: convergence from the flow's seam continuity h_charX_cont, domination from the Gronwall growth bound hC_T (Piece A) against f₀'s finite first moment. This is the structural reason h_cont_g does NOT need the general narrow→W₁ kernel — its consumer carries a pushforward representation.

theorem Vlasov.flowConv_continuousWithinAt_Ici_seam {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (charX : ℝ → PhaseSpace d → PhysSpace d) (f₀ : MeasureTheory.Measure (PhaseSpace d)) [MeasureTheory.IsProbabilityMeasure f₀] (hf₀_int : MeasureTheory.Integrable (fun (z : PhaseSpace d) => ‖z‖) f₀) {a b : ℝ} (hab : a < b) (μ : ℝ → MeasureTheory.Measure (PhysSpace d)) (h_push : ∀ s ∈ Set.Icc a b, μ s = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => charX s z) f₀) (h_aemeas : ∀ s ∈ Set.Icc a b, AEMeasurable (fun (z : PhaseSpace d) => charX s z) f₀) (h_charX_cont : ∀ (z : PhaseSpace d), ContinuousWithinAt (fun (s : ℝ) => charX s z) (Set.Ici a) a) (C_T : ℝ) (_hC_T_nn : 0 ≤ C_T) (hC_T : ∀ s ∈ Set.Icc a b, ∀ (z : PhaseSpace d), ‖charX s z‖ ≤ C_T * (‖z‖ + 1)) (z : PhaseSpace d) : ContinuousWithinAt (fun (s : ℝ) => convolveFunctionMeasure gradW (μ s) (charX s z)) (Set.Ici a) a

Route 2 inner kernel for glue_step h_cont_g (RIGHT / Ici a): the exact mirror of flowConv_continuousWithinAt_Iic_seam, but on Set.Ici a over a generic window [a, b] with the seam at the lower endpoint a. Same proof shape; the only set-dependent swaps are Iic T → Ici a, Icc_mem_nhdsLE → Icc_mem_nhdsGE, and the window [0, T] → [a, b]. Used for the RIGHT side of the seam at T where charX is the composed position flow Z_s z = charX_g (s-T) (charX_prev T z, …) and μ s = spatialMarginal (g (s-T)) is its pushforward of f₀.

theorem Vlasov.vlasovWellPosedness_glue {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_pos : 0 < T) (f_prev : ℝ → MeasureTheory.Measure (PhaseSpace d)) (h_prev_init : f_prev 0 = f₀) (h_prev_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f_prev t)) (hM_prev : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f_prev t) ≤ M) (charX_prev charV_prev : ℝ → PhaseSpace d → PhysSpace d) (h_prev_vlasov : IsVlasovSolutionOn gradW f_prev T) (h_prev_flow : IsCharacteristicFlowOn gradW (fun (t : ℝ) => spatialMarginal (f_prev t)) charX_prev charV_prev (Set.Ioo 0 T) Set.univ) (h_prev_push : ∀ t ∈ Set.Icc 0 T, f_prev t = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => (charX_prev t z, charV_prev t z)) (f_prev 0)) (h_prev_aemeas : ∀ s ∈ Set.Icc 0 T, AEMeasurable (fun (z : PhaseSpace d) => (charX_prev s z, charV_prev s z)) (f_prev 0)) (h_prev_boundary : ∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (fun (s : ℝ) => charX_prev s z) (charV_prev t z) (Set.Icc 0 T) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV_prev s z) (-convolveFunctionMeasure gradW (spatialMarginal (f_prev t)) (charX_prev t z)) (Set.Icc 0 T) t) (h_prev_ic : ∀ (z : PhaseSpace d), charX_prev 0 z = z.1 ∧ charV_prev 0 z = z.2) {T_0 : ℝ} (hT_0_pos : 0 < T_0) (hT_0_small_PL : LocalSmallnessPLBuffer L T_0) (hT_0_small_con : LocalSmallnessContraction L T_0) (hT_0_small_B : ↑L / (1 + ↑L) * (Real.exp ((1 + ↑L) * T_0) - 1) < 1) : ∃ (f_next : ℝ → MeasureTheory.Measure (PhaseSpace d)) (charX_next : ℝ → PhaseSpace d → PhysSpace d) (charV_next : ℝ → PhaseSpace d → PhysSpace d), (∀ t ∈ Set.Icc 0 T, f_next t = f_prev t) ∧ f_next 0 = f₀ ∧ (∀ t ∈ Set.Icc 0 (T + T_0), HasFiniteFirstMoment (f_next t)) ∧ (∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 (T + T_0), ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f_next t) ≤ M) ∧ IsLagrangianVlasovSolutionOn gradW f_next (T + T_0) ∧ (∀ t ∈ Set.Icc 0 (T + T_0), f_next t = MeasureTheory.Measure.map (fun (z : PhaseSpace d) => (charX_next t z, charV_next t z)) (f_next 0)) ∧ (∀ s ∈ Set.Icc 0 (T + T_0), AEMeasurable (fun (z : PhaseSpace d) => (charX_next s z, charV_next s z)) (f_next 0)) ∧ (∀ (z : PhaseSpace d), ∀ t ∈ Set.Icc 0 (T + T_0), HasDerivWithinAt (fun (s : ℝ) => charX_next s z) (charV_next t z) (Set.Icc 0 (T + T_0)) t ∧ HasDerivWithinAt (fun (s : ℝ) => charV_next s z) (-convolveFunctionMeasure gradW (spatialMarginal (f_next t)) (charX_next t z)) (Set.Icc 0 (T + T_0)) t) ∧ ∀ (z : PhaseSpace d), charX_next 0 z = z.1 ∧ charV_next 0 z = z.2

One-window glue step.

Given a solution f_prev : ℝ → Measure (PhaseSpace d) on [0, T] satisfying the local-existence conjuncts (initial condition + finite first moment + IsLagrangianVlasovSolutionOn), and a window length T_0 satisfying the smallness constraints LocalSmallnessPLBuffer L T_0 + LocalSmallnessContraction L T_0, produces a glued solution f_next : ℝ → Measure (PhaseSpace d) on [0, T + T_0] that agrees with f_prev on [0, T].

Proof strategy:

1. Shift the initial condition: apply vlasovWellPosedness_local to f_prev T (which has finite first moment by h_prev_mom T) with window length T_0. Gives a solution g : ℝ → Measure (PhaseSpace d) on [0, T_0] with g 0 = f_prev T.

2. Glue: define f_next t := if t ≤ T then f_prev t else g (t - T). Agreement at t = T is by g 0 = f_prev T.

3. Verify the four output conjuncts:

   • Initial: f_next 0 = f_prev 0 = f₀.
   • Moment: piecewise from h_prev_mom and g's moment bound.
   • IsLagrangianVlasovSolutionOn on [0, T + T_0]:
     • IsVlasovSolutionOn: weak PDE on Ioo 0 (T + T_0) — split at T, use h_prev_lag.1 for Ioo 0 T part and g's for Ioo T (T+T_0), continuity at T from the integral being continuous.
     • Flow: glue the per-window flows via standard ODE composition (charX_next(t, z) := if t ≤ T then charX_prev(t, z) else charX_g(t - T, (charX_prev(T, z), charV_prev(T, z)))).
     • Pushforward equation: holds piecewise.
     • AEMeasurable witness: composition of AEMeasurable maps.

theorem Vlasov.exists_localSmallness_window (L : NNReal) (hL_pos : 0 < ↑L) : ∃ (T_0 : ℝ), 0 < T_0 ∧ LocalSmallnessPLBuffer L T_0 ∧ LocalSmallnessContraction L T_0 ∧ ↑L / (1 + ↑L) * (Real.exp ((1 + ↑L) * T_0) - 1) < 1

For every positive Lipschitz constant there is a window length satisfying all three per-window smallness constraints — the PL buffer, the contraction, and the envelope closure. Pure threshold arithmetic: T_0 := min(1/√L, T_0_con, T_0_env)/2 with each threshold positive for every L > 0 (no L < 1 restriction).

theorem Vlasov.vlasovWellPosedness_forward {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) (hL_pos : 0 < ↑L) (f₀ : MeasureTheory.Measure (PhaseSpace d)) (hf₀ : HasFiniteFirstMoment f₀) {T_target : ℝ} (hT_target : 0 < T_target) : ∃ (f : ℝ → MeasureTheory.Measure (PhaseSpace d)), f 0 = f₀ ∧ (∀ t ∈ Set.Icc 0 T_target, HasFiniteFirstMoment (f t)) ∧ IsLagrangianVlasovSolutionOn gradW f T_target

Forward iteration to arbitrary T_target.

Extends the local-existence theorem from its small-T smallness window to any T_target > 0, by iterating the local theorem with shifted initial data at a fixed step T_0 depending only on L (no L < 1 hypothesis).

Proof strategy:

1. Pick T_0 := min(T_0_PL, T_0_con, T_0_env) / 2, with T_0_PL := 1/√L (the PL-buffer threshold for L · T_0² < 1), T_0_con/T_0_env the contraction/envelope thresholds. Each is positive for every L > 0, so T_0 > 0 and all three smallness constraints hold.

2. Pick N := ⌈T_target / T_0⌉₊ so that N · T_0 ≥ T_target.

3. Nat.rec construction: a solution holding the conjuncts at T = n·T_0.

   • Base case: apply vlasovWellPosedness_local directly.
   • Step case (n → n+1): apply vlasovWellPosedness_glue to extend.

4. Take f := f_N and verify the conjuncts for T_target ≤ N · T_0 via IsLagrangianVlasovSolutionOn's monotonicity in T (project down).