Compactly supported test approximation for weak Vlasov solutions

Mollification converges together with its first derivative. These estimates extend the weak equation to compactly supported C¹ tests, independently of flow inversion.

theorem Vlasov.mollifier_tendstoUniformly {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (g : PhaseSpace d → E) (hg_cont : Continuous g) (hg_cs : HasCompactSupport g) (φ : ℕ → ContDiffBump 0) (hφ : Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0)) : TendstoUniformly (fun (n : ℕ) (x : PhaseSpace d) => MeasureTheory.convolution ((φ n).normed MeasureTheory.volume) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x) g Filter.atTop

Helper 1 — uniform mollification of a continuous, compactly-supported function. The mollified family ρ_n ⋆ g converges to g uniformly (not just pointwise), the load-bearing analytic input the C¹_c test-class enlargement (#4) needs. Proof: uniform continuity of g (compact support) gives a single δ; once rOut_n < δ, the pointwise bump estimate dist_normed_convolution_le fires at every base point simultaneously.

theorem Vlasov.mollifiedFDeriv_tendstoUniformly {d : ℕ} (χ : PhaseSpace d → ℝ) (hχ_C1 : ContDiff ℝ 1 χ) (hχc : HasCompactSupport χ) (φ : ℕ → ContDiffBump 0) (hφ : Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0)) : TendstoUniformly (fun (n : ℕ) (z : PhaseSpace d) => fderiv ℝ (MeasureTheory.convolution ((φ n).normed MeasureTheory.volume) χ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) z) (fderiv ℝ χ) Filter.atTop

Helper 2 — the mollified Fréchet derivative converges uniformly. fderiv (ρ_n ⋆ χ) = ρ_n ⋆ (fderiv χ) (convolution commutes onto the C¹ factor via HasCompactSupport.hasFDerivAt_convolution_right, with precompR reconciled to lsmul on the operator codomain), and the right-hand side converges uniformly to fderiv χ by Helper 1 applied to the continuous, compactly-supported fderiv χ.

theorem Vlasov.toDualSymm_comp_sub_norm_le {d : ℕ} (ψ ϕ : PhaseSpace d → ℝ) (z : PhaseSpace d) (e : PhysSpace d →L[ℝ] PhaseSpace d) : ‖(InnerProductSpace.toDual ℝ (PhysSpace d)).symm (fderiv ℝ ψ z ∘SL e) - (InnerProductSpace.toDual ℝ (PhysSpace d)).symm (fderiv ℝ ϕ z ∘SL e)‖ ≤ ‖fderiv ℝ ψ z - fderiv ℝ ϕ z‖ * ‖e‖

Norm bound for the dual-composed difference of two Fréchet derivatives.

theorem Vlasov.fderiv_slice_fst {d : ℕ} (ψ : PhaseSpace d → ℝ) (hψ : Differentiable ℝ ψ) (z : PhaseSpace d) : fderiv ℝ (fun (x : PhysSpace d) => ψ (x, z.2)) z.1 = fderiv ℝ ψ z ∘SL ContinuousLinearMap.inl ℝ (PhysSpace d) (PhysSpace d)

Chain rule: the Fréchet derivative of an x-slice is the composition with inl.

theorem Vlasov.fderiv_slice_snd {d : ℕ} (ψ : PhaseSpace d → ℝ) (hψ : Differentiable ℝ ψ) (z : PhaseSpace d) : fderiv ℝ (fun (v : PhysSpace d) => ψ (z.1, v)) z.2 = fderiv ℝ ψ z ∘SL ContinuousLinearMap.inr ℝ (PhysSpace d) (PhysSpace d)

Chain rule: the Fréchet derivative of a v-slice is the composition with inr.

theorem Vlasov.continuous_gradientSlice_fst {d : ℕ} (ψ : PhaseSpace d → ℝ) (g : PhaseSpace d → PhysSpace d) (hψ : Differentiable ℝ ψ) (hψ' : Continuous (fderiv ℝ ψ)) (hg : ∀ (z : PhaseSpace d), g z = gradient (fun (x : PhysSpace d) => ψ (x, z.2)) z.1) : Continuous g

Continuity of the first-slot partial-gradient field of a C¹ test function.

theorem Vlasov.continuous_gradientSlice_snd {d : ℕ} (ψ : PhaseSpace d → ℝ) (g : PhaseSpace d → PhysSpace d) (hψ : Differentiable ℝ ψ) (hψ' : Continuous (fderiv ℝ ψ)) (hg : ∀ (z : PhaseSpace d), g z = gradient (fun (v : PhysSpace d) => ψ (z.1, v)) z.2) : Continuous g

Continuity of the second-slot partial-gradient field of a C¹ test function.

theorem Vlasov.hasCompactSupport_gradientSlice_fst {d : ℕ} (ψ : PhaseSpace d → ℝ) (g : PhaseSpace d → PhysSpace d) (hψ : Differentiable ℝ ψ) (hψcs : HasCompactSupport ψ) (hg : ∀ (z : PhaseSpace d), g z = gradient (fun (x : PhysSpace d) => ψ (x, z.2)) z.1) : HasCompactSupport g

Compact support of the first-slot partial-gradient field.

theorem Vlasov.hasCompactSupport_gradientSlice_snd {d : ℕ} (ψ : PhaseSpace d → ℝ) (g : PhaseSpace d → PhysSpace d) (hψ : Differentiable ℝ ψ) (hψcs : HasCompactSupport ψ) (hg : ∀ (z : PhaseSpace d), g z = gradient (fun (v : PhysSpace d) => ψ (z.1, v)) z.2) : HasCompactSupport g

Compact support of the second-slot partial-gradient field.

theorem Vlasov.gradientSlice_fst_sub_norm_le {d : ℕ} (ψ ϕ : PhaseSpace d → ℝ) (hψ : Differentiable ℝ ψ) (hϕ : Differentiable ℝ ϕ) (gψ gϕ : PhaseSpace d → PhysSpace d) (hgψ : ∀ (z : PhaseSpace d), gψ z = gradient (fun (x : PhysSpace d) => ψ (x, z.2)) z.1) (hgϕ : ∀ (z : PhaseSpace d), gϕ z = gradient (fun (x : PhysSpace d) => ϕ (x, z.2)) z.1) (z : PhaseSpace d) : ‖gψ z - gϕ z‖ ≤ ‖fderiv ℝ ψ z - fderiv ℝ ϕ z‖

First-slot partial gradients of two tests differ by at most the full Fréchet-derivative difference.

theorem Vlasov.gradientSlice_snd_sub_norm_le {d : ℕ} (ψ ϕ : PhaseSpace d → ℝ) (hψ : Differentiable ℝ ψ) (hϕ : Differentiable ℝ ϕ) (gψ gϕ : PhaseSpace d → PhysSpace d) (hgψ : ∀ (z : PhaseSpace d), gψ z = gradient (fun (v : PhysSpace d) => ψ (z.1, v)) z.2) (hgϕ : ∀ (z : PhaseSpace d), gϕ z = gradient (fun (v : PhysSpace d) => ϕ (z.1, v)) z.2) (z : PhaseSpace d) : ‖gψ z - gϕ z‖ ≤ ‖fderiv ℝ ψ z - fderiv ℝ ϕ z‖

Second-slot partial gradients of two tests differ by at most the full Fréchet-derivative difference.

theorem Vlasov.inner_integrand_integrable {d : ℕ} (μ : MeasureTheory.Measure (PhaseSpace d)) [MeasureTheory.IsProbabilityMeasure μ] (fld : PhysSpace d → PhysSpace d) (hfld : Continuous fld) (gX gV : PhaseSpace d → PhysSpace d) (hgXc : Continuous gX) (hgVc : Continuous gV) (hgXcs : HasCompactSupport gX) (hgVcs : HasCompactSupport gV) : MeasureTheory.Integrable (fun (z : PhaseSpace d) => inner ℝ z.2 (gX z) - inner ℝ (fld z.1) (gV z)) μ

Integrability of the weak-evolution integrand against a probability measure: continuous with compact support (both gradient slots), continuous field.

theorem Vlasov.inner_integrand_sub_norm_le {d : ℕ} (K : Set (PhaseSpace d)) (R_K : ℝ) (hR_K_nn : 0 ≤ R_K) (hR_K : ∀ z ∈ K, ‖z‖ ≤ R_K) (fld : PhysSpace d → PhysSpace d) (B : ℝ) (hB_nn : 0 ≤ B) (hfld_K : ∀ z ∈ K, ‖fld z.1‖ ≤ B) (gX gV gX' gV' : PhaseSpace d → PhysSpace d) (δ : ℝ) (hδ_nn : 0 ≤ δ) (hXd : ∀ (z : PhaseSpace d), ‖gX' z - gX z‖ ≤ δ) (hVd : ∀ (z : PhaseSpace d), ‖gV' z - gV z‖ ≤ δ) (hXoff : ∀ z ∉ K, gX' z = gX z) (hVoff : ∀ z ∉ K, gV' z = gV z) (z : PhaseSpace d) : ‖inner ℝ z.2 (gX z) - inner ℝ (fld z.1) (gV z) - (inner ℝ z.2 (gX' z) - inner ℝ (fld z.1) (gV' z))‖ ≤ (R_K + B) * δ

Pointwise bound on the difference of two weak-evolution integrands: on the common support K it is (R_K + B) * δ (norm bound R_K on K, field bound B on K, gradient-slot distance δ); off K both integrands agree.

theorem Vlasov.convolveField_window_setup {d : ℕ} (gradW : PhysSpace d → PhysSpace d) (L : NNReal) (hL : LipschitzWith L gradW) (f : ℝ → MeasureTheory.Measure (PhaseSpace d)) (T : ℝ) (hf_mom : ∀ t ∈ Set.Icc 0 T, HasFiniteFirstMoment (f t)) (M_ρ : ℝ) (hM_ρ : ∀ t ∈ Set.Icc 0 T, ∫ (y : PhysSpace d), ‖y‖ ∂spatialMarginal (f t) ≤ M_ρ) (ε₀ : ℝ) (hε₀_def : ε₀ = ‖gradW 0‖ + ↑L * M_ρ) (σ : ℝ) : σ ∈ Set.Icc 0 T → MeasureTheory.Integrable (fun (y : PhysSpace d) => ‖y‖) (spatialMarginal (f σ)) ∧ (∀ (x : PhysSpace d), MeasureTheory.Integrable (fun (y : PhysSpace d) => gradW (x - y)) (spatialMarginal (f σ))) ∧ (∀ (x : PhysSpace d), ‖convolveFunctionMeasure gradW (spatialMarginal (f σ)) x‖ ≤ ε₀ + ↑L * ‖x‖) ∧ Continuous fun (x : PhysSpace d) => convolveFunctionMeasure gradW (spatialMarginal (f σ)) x

On the window, the frozen convolution field over the spatial marginal is integrable (in force form), linearly bounded, and continuous — packaged for consumers that quantify over the window.

theorem Vlasov.integral_tendsto_of_tendstoUniformly {d : ℕ} (μ : MeasureTheory.Measure (PhaseSpace d)) [MeasureTheory.IsProbabilityMeasure μ] (g : ℕ → PhaseSpace d → ℝ) (g₀ : PhaseSpace d → ℝ) (hUnif : TendstoUniformly g g₀ Filter.atTop) (hg₀_int : MeasureTheory.Integrable g₀ μ) (hg_int : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : PhaseSpace d), g n z ∂μ) Filter.atTop (nhds (∫ (z : PhaseSpace d), g₀ z ∂μ))

Uniform convergence of integrands implies convergence of the integrals against a probability measure (every term integrable).

theorem Vlasov.weakEvolution_test_C1c_On {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)) (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_ρ) (χ : PhaseSpace d → ℝ) (hχ_C1 : ContDiff ℝ 1 χ) (hχc : HasCompactSupport χ) (gradXχ gradVχ : PhaseSpace d → PhysSpace d) (hgradXχ : ∀ (z : PhaseSpace d), gradXχ z = gradient (fun (x : PhysSpace d) => χ (x, z.2)) z.1) (hgradVχ : ∀ (z : PhaseSpace d), gradVχ z = gradient (fun (v : PhysSpace d) => χ (z.1, v)) z.2) (s : ℝ) (hs : s ∈ Set.Ioo 0 T) : HasDerivAt (fun (σ : ℝ) => ∫ (z : PhaseSpace d), χ z ∂f σ) (∫ (z : PhaseSpace d), inner ℝ z.2 (gradXχ z) - inner ℝ (convolveFunctionMeasure gradW (spatialMarginal (f s)) z.1) (gradVχ z) ∂f s) s

theorem Vlasov.vlasovSolutionOn_integral_continuousOn {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)) (G : ℝ → PhaseSpace d → ℝ) (hG_cont : Continuous fun (p : ℝ × PhaseSpace d) => G p.1 p.2) (K : Set (PhaseSpace d)) (hK : IsCompact K) (hG_supp : ∀ (s : ℝ), ∀ z ∉ K, G s z = 0) : ContinuousOn (fun (s : ℝ) => ∫ (z : PhaseSpace d), G s z ∂f s) (Set.Icc 0 T)