set_option linter.style.longLine false

PSD Helpers: Continuity and Pointwise Bounds for Coulomb

Proves the Landau quadratic form bound, continuity of the PSD integrand (the Coulomb singularity cancels in the quadratic form), and pointwise bounds. These are building blocks for the integrability and Fubini results in CoulombPSD.

theorem VML.landau_bound (z u : Fin 3 → ℝ) : |u ⬝ᵥ (landauMatrix coulombKernel z).mulVec u| ≤ (if eucNorm z = 0 then 0 else (eucNorm z)⁻¹) * eucNorm u ^ 2

theorem VML.tendsto_landau_quadratic_diag (G : (Fin 3 → ℝ) → Fin 3 → ℝ) (hG : ContDiff ℝ 1 G) (x : Fin 3 → ℝ) : Filter.Tendsto (fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => (G p.1 - G p.2) ⬝ᵥ (landauMatrix coulombKernel (p.1 - p.2)).mulVec (G p.1 - G p.2)) (nhds (x, x)) (nhds 0)

theorem VML.continuous_landau_quadratic (G : (Fin 3 → ℝ) → Fin 3 → ℝ) (hG : ContDiff ℝ 1 G) : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => (G p.1 - G p.2) ⬝ᵥ (landauMatrix coulombKernel (p.1 - p.2)).mulVec (G p.1 - G p.2)

theorem VML.psd_continuous_coulomb (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand coulombKernel f p.1 p.2

PSD integrand is jointly continuous for Coulomb kernel. Despite Ψ(r) = r⁻³ being singular, the score difference cancels the singularity. Proved by Aristotle (job 14300a69). Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

theorem VML.psd_pointwise_bound_coulomb (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) {Cg : ℝ} {Kg : ℕ} (h_score : ∀ (u : Fin 3 → ℝ) (i : Fin 3), |vGrad (Real.log ∘ f) u i| ≤ Cg * (1 + ‖u‖) ^ Kg) (v w : Fin 3 → ℝ) : |PSDIntegrand coulombKernel f v w| ≤ 18 * Cg ^ 2 * f v * ((1 + ‖v‖) ^ (2 * Kg) * (‖v - w‖⁻¹ * f w) + ‖v - w‖⁻¹ * ((1 + ‖w‖) ^ (2 * Kg) * f w))

Pointwise bound on PSD integrand for Coulomb kernel: |PSD(v,w)| ≤ 18Cg²f(v) * ((1+‖v‖)^{2Kg}·‖v-w‖⁻¹f(w) + ‖v-w‖⁻¹·(1+‖w‖)^{2Kg}f(w))

theorem VML.fubini_double_pointwise_bound {f : (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) {Cg : ℝ} {Kg : ℕ} (h_score : ∀ (u : Fin 3 → ℝ) (i : Fin 3), |vGrad (Real.log ∘ f) u i| ≤ Cg * (1 + ‖u‖) ^ Kg) (v w : Fin 3 → ℝ) : |vGrad (Real.log ∘ f) v ⬝ᵥ (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)| ≤ 3 * Cg * (1 + ‖v‖) ^ Kg * (‖v - w‖⁻¹ * ∑ j : Fin 3, (f w * |vGrad f v j| + f v * |vGrad f w j|))

Pointwise bound on the Fubini double integrand for Coulomb. |score(v) · (A(v-w) · flux(v,w))| ≤ 3Cg(1+‖v‖)^Kg * ‖v-w‖⁻¹ * Σ_j (...).

theorem VML.fubini_double_aestronglyMeasurable {f : (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) : MeasureTheory.AEStronglyMeasurable (fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => vGrad (Real.log ∘ f) p.1 ⬝ᵥ (landauMatrix coulombKernel (p.1 - p.2)).mulVec (f p.2 • vGrad f p.1 - f p.1 • vGrad f p.2)) (MeasureTheory.volume.prod MeasureTheory.volume)

The Fubini double integrand (score · Landau matrix · flux) is AEStronglyMeasurable on the product space (Fin 3 → ℝ) × (Fin 3 → ℝ).