set_option linter.style.longLine false

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) : ∃ Cf > 0, ∀ (v : Fin 3 → ℝ), |(∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)) i| ≤ Cf * g v * (1 + ‖v‖) ^ Kg

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) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) i * (fderiv ℝ (Real.log ∘ f) v) (Pi.single i 1)) MeasureTheory.volume

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.