Force Transport and IBP Integrability for Coulomb

Proves integrability of the spatial transport term (v · ∇ₓf · log f), force transport term ((E + v × B) · ∇ᵥf · log f), and force IBP terms for the Coulomb kernel. Uses Schwartz decay, log growth bounds, and the Lorentz force component bound.

theorem VML.torusGradX_aestronglyMeasurable {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.AEStronglyMeasurable (fun (v : Fin 3 → ℝ) => torusGradX (fun (y : Torus3) => f y v) x i) MeasureTheory.volume

Spatial gradient of f w.r.t. x is AEStronglyMeasurable in v, via difference quotient limits.

theorem VML.spatial_transport_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) (x : Torus3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => v ⬝ᵥ FlatTorus3.gradX (fun (y : Torus3) => f y v) x * Real.log (f x v)) MeasureTheory.volume

Spatial transport integrand is dominated by inverse polynomial (from Schwartz grad decay + log bound).

theorem VML.force_fderiv_log_component_integrable {f : Torus3 → (Fin 3 → ℝ) → ℝ} (E B : Torus3 → Fin 3 → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hSchwartz : UniformSchwartzDecay f) (C_log : ℝ) (K_log : ℕ) (hLB : ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) (x : Torus3) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) i * (fderiv ℝ (f x) v) (Pi.single i 1) * Real.log (f x v)) MeasureTheory.volume

Each force × fderiv × log component is integrable (shared helper for force_transport and force_ibp_f_dg).

theorem VML.force_transport_integrable_coulomb {f : Torus3 → (Fin 3 → ℝ) → ℝ} (E B : Torus3 → Fin 3 → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) (x : Torus3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v * Real.log (f x v)) MeasureTheory.volume

Force transport integrand is integrable (from Schwartz derivative decay + log bound + Lorentz bound).

theorem VML.force_ibp_f_dg_integrable_coulomb {f : Torus3 → (Fin 3 → ℝ) → ℝ} (E B : Torus3 → Fin 3 → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) (x : Torus3) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) i * (fderiv ℝ (fun (w : Fin 3 → ℝ) => f x w * Real.log (f x w) - f x w) v) (Pi.single i 1)) MeasureTheory.volume

Force IBP (f·dg form) integrand is integrable. Uses chain rule: d/dv(f·log f - f) = f'·log f.

theorem VML.force_ibp_fg_integrable_coulomb {f : Torus3 → (Fin 3 → ℝ) → ℝ} (E B : Torus3 → Fin 3 → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hSchwartz : UniformSchwartzDecay f) (hLogBound : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log) (x : Torus3) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) i * (f x v * Real.log (f x v) - f x v)) MeasureTheory.volume

Force IBP (f·g form) integrand is integrable.