Gaussian Helper Lemmas

Gaussian normalization, gradient of exponential-quadratic functions, integrability, and related analysis lemmas used in Section 3.

theorem VML.vGrad_exp_quadratic (a : ℝ) (b : Fin 3 → ℝ) (c : ℝ) (v : Fin 3 → ℝ) : vGrad (fun (w : Fin 3 → ℝ) => Real.exp (a + b ⬝ᵥ w + c * normSq w)) v = Real.exp (a + b ⬝ᵥ v + c * normSq v) • (b + (2 * c) • v)

The velocity gradient of exp(a + b·v + c·|v|²) equals exp(a + b·v + c·|v|²)·(b + 2c·v). Proved by Aristotle (Harmonic).

theorem VML.gaussian_normalization_maxwellian (ρ_ion a₀ c₀ : ℝ) (hρ : 0 < ρ_ion) (hc₀ : c₀ < 0) (f : (Fin 3 → ℝ) → ℝ) (hf : ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + c₀ * normSq v)) (hf_int : ∫ (v : Fin 3 → ℝ), f v = ρ_ion) (v : Fin 3 → ℝ) : f v = equilibriumMaxwellian ρ_ion (-1 / (2 * c₀)) v

Gaussian normalization: if f(v) = exp(a₀ + c₀|v|²) with c₀ < 0 and ∫f = ρ_ion, then f = equilibriumMaxwellian ρ_ion T with T = -1/(2c₀). Proved by Aristotle (project 1236b757).

theorem VML.gaussian_first_moment (a : ℝ) (b : Fin 3 → ℝ) (c : ℝ) (hc : c < 0) (hf_int : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => Real.exp (a + b ⬝ᵥ v + c * normSq v)) MeasureTheory.volume) (i : Fin 3) : ∫ (v : Fin 3 → ℝ), v i * Real.exp (a + b ⬝ᵥ v + c * normSq v) = -b i / (2 * c) * ∫ (v : Fin 3 → ℝ), Real.exp (a + b ⬝ᵥ v + c * normSq v)

Gaussian first moment: ∫ vᵢ exp(a+b·v+c|v|²) = (-bᵢ/(2c)) · ∫ exp(a+b·v+c|v|²). Proved by Aristotle (project 4c5e7998).

theorem VML.analysis_gaussian_integrability (f : (Fin 3 → ℝ) → ℝ) (a₀ : ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hf_exp : ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + b ⬝ᵥ v + c₀ * normSq v)) : c₀ < 0

Gaussian integrability: exp(a₀+b·v+c₀|v|²) with f integrable implies c₀ < 0.

theorem VML.analysis_vGrad_smooth (g : (Fin 3 → ℝ) → ℝ) (hg : ContDiff ℝ 3 g) : ContDiff ℝ 2 fun (v : Fin 3 → ℝ) => vGrad g v

Smoothness of velocity gradient: if g is smooth, so is vGrad g.

theorem VML.cubic_coeff_zero (a : Fin 3 → ℝ) (h : ∀ (v : Fin 3 → ℝ), v ⬝ᵥ a * normSq v = 0) : a = 0

Gap 12: (v · a) |v|² = 0 for all v ∈ ℝ³ implies a = 0. Choose v = t eᵢ, divide by t³, let t → ∞. Reference: Step in the proof of Lemma 14 (lem:T_constant).

theorem VML.poisson_boltzmann_max_principle (X : Type u_1) [Nonempty X] (n : X → ℝ) (ρ_ion T_infty : ℝ) (laplacian : (X → ℝ) → X → ℝ) (_hn_pos : ∀ (x : X), 0 < n x) (hT : 0 < T_infty) (_hρ : 0 < ρ_ion) (hPB : ∀ (x : X), T_infty * laplacian (Real.log ∘ n) x = n x - ρ_ion) (x_max : X) (hmax : ∀ (x : X), n x ≤ n x_max) (x_min : X) (hmin : ∀ (x : X), n x_min ≤ n x) (hmax_lapl : laplacian (Real.log ∘ n) x_max ≤ 0) (hmin_lapl : 0 ≤ laplacian (Real.log ∘ n) x_min) (x : X) : n x = ρ_ion

Gap 15: Maximum principle for the Poisson–Boltzmann equation on T³. If T∞ Δ(log n) = n - ρ_ion with T∞ > 0 and n > 0, then n ≡ ρ_ion. At the maximum of n: Δ(log n) ≤ 0 → n ≤ ρ_ion. At the minimum: Δ(log n) ≥ 0 → n ≥ ρ_ion. Reference: Proof of Lemma 21 (lem:density_constant).

theorem VML.current_density_of_gaussian (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (a₀ : ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (hform : ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + b ⬝ᵥ v + c₀ * normSq v)) (i : Fin 3) : ∫ (v : Fin 3 → ℝ), v i * f v = (∫ (v : Fin 3 → ℝ), f v) * (-1 / (2 * c₀) * b i)

If f equals a Gaussian exp(a₀ + b·v + c₀|v|²), then the first moment ∫ vᵢ f(v) equals (∫ f(v)) * (-1/(2c₀)) * bᵢ.