Gaussian representations of the Coulomb kernel

Equation, including the infinite diagonal.

Pointwise completion of squares, prior to integration.

theorem LiebThirring.measurable_coulombKernel : Measurable (Function.uncurry coulombKernel)

theorem LiebThirring.coulombKernel_symm (x y : Position) : coulombKernel x y = coulombKernel y x

theorem LiebThirring.inverse_eq_lintegral_gaussian (s : ℝ) (hs : 0 ≤ s) : (ENNReal.ofReal s)⁻¹ = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (2 / √Real.pi * Real.exp (-(t ^ 2 * s ^ 2)))

theorem LiebThirring.coulombKernel_eq_lintegral_gaussian (x y : Position) : coulombKernel x y = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (2 / √Real.pi * Real.exp (-(t ^ 2 * ‖x - y‖ ^ 2)))

Equation (2.1), including the infinite diagonal.

theorem LiebThirring.norm_midpoint_sq (x y z : Position) : ‖x - z‖ ^ 2 + ‖y - z‖ ^ 2 = 2 * ‖z - (1 / 2) • (x + y)‖ ^ 2 + ‖x - y‖ ^ 2 / 2

theorem LiebThirring.gaussian_product_eq (b : ℝ) (x y z : Position) : Real.exp (-2 * b * ‖x - z‖ ^ 2) * Real.exp (-2 * b * ‖y - z‖ ^ 2) = Real.exp (-b * ‖x - y‖ ^ 2) * Real.exp (-(4 * b) * ‖z - (1 / 2) • (x + y)‖ ^ 2)

Pointwise completion of squares, prior to integration.

theorem LiebThirring.integral_gaussian_product (b : ℝ) (hb : 0 < b) (x y : Position) : ∫ (z : Position), Real.exp (-2 * b * ‖x - z‖ ^ 2) * Real.exp (-2 * b * ‖y - z‖ ^ 2) = Real.exp (-b * ‖x - y‖ ^ 2) * (Real.pi / (4 * b)) ^ (3 / 2)

theorem LiebThirring.integrable_gaussian_norm {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (z : Position) => Real.exp (-b * ‖z‖ ^ 2)) MeasureTheory.volume

theorem LiebThirring.integrable_gaussian_product {b : ℝ} (hb : 0 < b) (x y : Position) : MeasureTheory.Integrable (fun (z : Position) => Real.exp (-2 * b * ‖x - z‖ ^ 2) * Real.exp (-2 * b * ‖y - z‖ ^ 2)) MeasureTheory.volume

Absolute integrability of the product in (2.2).

noncomputable def LiebThirring.gaussianMass (b : ℝ) : ℝ

Spatial Gaussian convolution mass in three Euclidean dimensions.

Equations

• LiebThirring.gaussianMass b = (Real.pi / (4 * b)) ^ (3 / 2)

noncomputable def LiebThirring.gaussianFeature (c b : ℝ) (x z : Position) : ENNReal

A nonnegative Gaussian feature with scalar normalization c.

Equations

• LiebThirring.gaussianFeature c b x z = ENNReal.ofReal (√(c / LiebThirring.gaussianMass b) * Real.exp (-2 * b * ‖x - z‖ ^ 2))

theorem LiebThirring.sqrt_mul_sqrt_mul (a u v : ℝ) (ha : 0 ≤ a) : √a * u * (√a * v) = a * (u * v)

Cancellation of the square root normalization.

theorem LiebThirring.lintegral_gaussianFeature_mul {b c : ℝ} (hb : 0 < b) (hc : 0 ≤ c) (x y : Position) : ∫⁻ (z : Position), gaussianFeature c b x z * gaussianFeature c b y z = ENNReal.ofReal (c * Real.exp (-b * ‖x - y‖ ^ 2))

Integral Gram representation of a Gaussian kernel.