theorem VML.gradX_stronglyMeasurable_v (f : Torus3 → (Fin 3 → ℝ) → ℝ) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (x : Torus3) (i : Fin 3) : MeasureTheory.StronglyMeasurable fun (v : Fin 3 → ℝ) => FlatTorus3.gradX (fun (y : Torus3) => f y v) x i

The spatial gradient component v ↦ gradX(fun y => f y v)(x)(i) is strongly measurable in v. Proved via difference quotient approximation: each quotient is continuous in v (since f(x,·) is smooth for each torus point), and the fderiv is their pointwise limit.

theorem VML.spatial_transport_joint_integrable {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) : MeasureTheory.Integrable (Function.uncurry fun (x : Torus3) (v : Fin 3 → ℝ) => v ⬝ᵥ FlatTorus3.gradX (fun (y : Torus3) => f y v) x * Real.log (f x v)) (MeasureTheory.volume.prod MeasureTheory.volume)

Spatial transport joint integrability (Fubini on compact torus × ℝ³). Uses: uniform Schwartz grad decay → uniform velocity integral bound, combined with finite measure on compact T³ → joint integrability.

theorem VML.spatial_transport_continuous {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) : Continuous fun (x : Torus3) => ∫ (v : Fin 3 → ℝ), v ⬝ᵥ FlatTorus3.gradX (fun (y : Torus3) => f y v) x * Real.log (f x v)

The parametric integral x ↦ ∫ v, v ⬝ᵥ gradX(f)(x) * log(f(x,v)) is continuous on the torus. Proved via continuous_of_dominated using the uniform Schwartz+log bound from spatial_transport_joint_integrable.

theorem VML.entropy_dissipation_continuous_coulomb (f : Torus3 → (Fin 3 → ℝ) → ℝ) (E B : Torus3 → Fin 3 → ℝ) (ν : ℝ) (hν : 0 < ν) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C : ℝ) (K : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C * (1 + ‖v‖) ^ K) (hVlasov : ∀ (x : Torus3) (v : Fin 3 → ℝ), v ⬝ᵥ torusGradX (fun (y : Torus3) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator coulombKernel (f x) v) : Continuous fun (x : Torus3) => entropyDissipation coulombKernel (f x)

Continuity of entropy dissipation for the Coulomb kernel. Derives from the Vlasov equation: force transport vanishes by IBP, so D(f x) = ν⁻¹ ∫ spatial·log f, which is continuous by spatial_transport_continuous.