Flux Component Bounds and Flux × Log Integrability for Coulomb #
Proves:
flux_times_log_integrable_coulomb: The flux × log(f) product is integrable.coulomb_flux_component_bound: Pointwise |flux_i(v)| ≤ Cf * g(v) * (1+‖v‖)^Kg.
theorem
VML.flux_times_log_integrable_coulomb
{f : Torus3 → (Fin 3 → ℝ) → ℝ}
(hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v)
(hf_smooth_v : ∀ (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 → ℝ) =>
(∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) i * (Real.log ∘ f x) v)
MeasureTheory.volume
The Landau flux × log(f) is integrable for the Coulomb kernel. Uses the uniform Newtonian bound to control the flux pointwise.
theorem
VML.coulomb_flux_component_bound
(g : (Fin 3 → ℝ) → ℝ)
(hg_pos : ∀ (v : Fin 3 → ℝ), 0 < g v)
(hg_smooth : ContDiff ℝ 3 g)
(hg_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k g v‖ * (1 + ‖v‖) ^ N ≤ C)
{Cg : ℝ}
{Kg : ℕ}
(hGrad : ∀ (v : Fin 3 → ℝ) (j : Fin 3), |(fderiv ℝ g v) (Pi.single j 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * g v)
(i : Fin 3)
:
Pointwise bound on the Coulomb flux component: |flux_i(v)| ≤ Cf * g(v) * (1+‖v‖)^Kg. Combines the Newtonian potential bound (∫ ‖v-w‖⁻¹ |g| ≤ M) with the polynomial gradient bound |∂_j g(v)| ≤ Cg * (1+‖v‖)^Kg * g(v).
theorem
VML.coulomb_ibp_f_dg_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)
{Cg : ℝ}
{Kg : ℕ}
(hGrad : ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ f v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f v)
(i : Fin 3)
:
The product flux_i(v) * score_i(v) is integrable for the Coulomb kernel. Uses coulomb_flux_component_bound (|flux_i| ≤ Cff(1+‖v‖)^Kg) and score_bound_of_grad_bound (|score_i| ≤ Cg*(1+‖v‖)^Kg), giving a CfCg(1+‖v‖)^{2Kg}*f(v) dominator which is integrable by Schwartz decay.