theorem VML.coulomb_flux_deriv_schwartz_decay (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (i : Fin 3) (N : ℕ) : ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖fderiv ℝ (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) i) v‖ * (1 + ‖v‖) ^ N ≤ C

The derivative of the Coulomb flux component has Schwartz-class decay. Since the flux decomposes into convolutions of Coulomb entries with Schwartz functions, its derivatives inherit Schwartz decay via coulomb_entry_conv_deriv_decay.

theorem VML.coulomb_ibp_df_g_integrable (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (hLogBound : ∃ (C : ℝ) (K : ℕ), ∀ (v : Fin 3 → ℝ), |Real.log (f v)| ≤ C * (1 + ‖v‖) ^ K) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (fderiv ℝ (fun (v' : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v' - w)).mulVec (f w • vGrad f v' - f v' • vGrad f w)) i) v) (Pi.single i 1) * (Real.log ∘ f) v) MeasureTheory.volume

The product fderiv(flux_i)(v) * log(f(v)) is integrable for the Coulomb kernel. Uses Schwartz decay of the flux derivative and polynomial growth of log(f).