set_option linter.style.longLine false

Coulomb Entry Convolution: Differentiability and Bounds

Establishes that partial derivatives of functions with C² decay are C² decay, Coulomb kernel entry convolutions are differentiable with uniform derivative bounds, and the full Coulomb flux component is differentiable with a decomposition formula.

theorem VML.schwartz_fderiv_component_schwartz (f : (Fin 3 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ 3 f) (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (j : Fin 3) (N : ℕ) {k : ℕ} (hk : k + 1 ≤ 2) : ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k (fun (w : Fin 3 → ℝ) => (fderiv ℝ f w) (Pi.single j 1)) v‖ * (1 + ‖v‖) ^ N ≤ C

Partial derivatives of a Schwartz function are Schwartz. Uses ContinuousLinearMap.iteratedFDeriv_comp_left + norm_iteratedFDeriv_fderiv.

theorem VML.coulomb_entry_schwartz_integrable (g : (Fin 3 → ℝ) → ℝ) (hg_smooth : ContDiff ℝ 2 g) (hg_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (v : Fin 3 → ℝ), |g v| * (1 + ‖v‖) ^ N ≤ C) (v : Fin 3 → ℝ) (i j : Fin 3) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => landauMatrix coulombKernel (v - w) i j * g w) MeasureTheory.volume

Coulomb matrix entry times Schwartz function is integrable in ℝ³. Domination: |A_{ij}(v-w) * g(w)| ≤ ‖v-w‖⁻¹ * |g(w)| by entry bound.

theorem VML.coulomb_entry_conv_differentiable (g : (Fin 3 → ℝ) → ℝ) (hg_smooth : ContDiff ℝ 2 g) (hg_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 1 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k g v‖ * (1 + ‖v‖) ^ N ≤ C) (i j : Fin 3) : Differentiable ℝ fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), landauMatrix coulombKernel (v - w) i j * g w

theorem VML.coulomb_entry_conv_deriv_bounded (g : (Fin 3 → ℝ) → ℝ) (hg_smooth : ContDiff ℝ 2 g) (hg_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 1 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k g v‖ * (1 + ‖v‖) ^ N ≤ C) (i j : Fin 3) : ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖fderiv ℝ (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), landauMatrix coulombKernel (v - w) i j * g w) v‖ ≤ C

The derivative of a Coulomb entry convolution with a Schwartz function is uniformly bounded. After substituting u = v - w, the fderiv acts only on g(v-u), giving fderiv(conv)(v) = ∫ A(u) • fderiv(g)(v-u) du. The bound follows from |A(u)| ≤ ‖u‖⁻¹ and integrability of ‖u‖⁻¹ * ‖fderiv g(·)‖ via newtonian_schwartz_uniform_bound.

NOTE: The convolution does NOT have Schwartz decay (only O(‖v‖⁻²) since the Coulomb kernel is degree -1 homogeneous). But the uniform bound suffices because in coulomb_flux_deriv_schwartz_decay, convolution derivatives are multiplied by Schwartz-decaying factors (f, ∂_j f).

theorem VML.coulomb_flux_differentiable (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) : Differentiable ℝ fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) i

The Coulomb flux component v ↦ (∫_w A(v-w)·[f(w)∇f(v)-f(v)∇f(w)])_i is differentiable.

Proof strategy: Decompose the flux as flux_i(v) = Σ_j (∂j f)(v) * K{ij}(v) - f(v) * Σ_j L_{ij}(v) where K_{ij}(v) = ∫ A_{ij}(v-w) f(w) dw and L_{ij}(v) = ∫ A_{ij}(v-w) (∂j f)(w) dw. Each K{ij} and L_{ij} is differentiable by coulomb_entry_conv_differentiable. Then flux_i is differentiable by product/sum rules.

theorem VML.coulomb_flux_eq_decomposed (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) (v : Fin 3 → ℝ) : (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) i = ∑ j : Fin 3, (((fderiv ℝ f v) (Pi.single j 1) * ∫ (w : Fin 3 → ℝ), landauMatrix coulombKernel (v - w) i j * f w) - f v * ∫ (w : Fin 3 → ℝ), landauMatrix coulombKernel (v - w) i j * (fderiv ℝ f w) (Pi.single j 1))

The Coulomb flux component equals the K/L decomposition pointwise: (∫ w, mulVec A(v-w) (f(w)•∇f(v) - f(v)•∇f(w)))i = Σ_j [∂j f(v) * K_j(v) - f(v) * L_j(v)] where K_j(v) = ∫ A{ij}(v-w) f(w) dw and L_j(v) = ∫ A{ij}(v-w) ∂_j f(w) dw.

theorem VML.coulomb_entry_conv_uniform_bound {g : (Fin 3 → ℝ) → ℝ} (hg_decay : ∀ (M : ℕ), ∃ C > 0, ∀ (w : Fin 3 → ℝ), |g w| * (1 + ‖w‖) ^ M ≤ C) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (i j : Fin 3) : ∃ M > 0, ∀ (v : Fin 3 → ℝ), |∫ (w : Fin 3 → ℝ), landauMatrix coulombKernel (v - w) i j * g w| ≤ M

Coulomb convolution of a Schwartz-decaying function is uniformly bounded: |∫ A_{ij}(v-w) * g(w) dw| ≤ M for all v. Uses |A_{ij}(z)| ≤ ‖z‖⁻¹ and the Newtonian potential uniform bound.