set_option linter.style.longLine false
Poisson-Boltzmann and Electric Field (Section 7) #
Derives the Poisson-Boltzmann equation from force balance and Gauss's law, then proves the electric field vanishes (E = 0) and the magnetic field is spatially constant using harmonic function theory on the torus.
theorem
VML.poisson_boltzmann_algebraic
{X : Type u_1}
(gradX : (X → ℝ) → X → Fin 3 → ℝ)
(divX : (X → Fin 3 → ℝ) → X → ℝ)
(E : X → Fin 3 → ℝ)
(ρ : X → ℝ)
(ρ_ion : ℝ)
(a₀ : X → ℝ)
(c₀ : ℝ)
(_hc₀ : c₀ < 0)
(hForce : ∀ (x : X), gradX a₀ x = (-2 * c₀) • E x)
(hGradLogRho : ∀ (x : X), gradX (Real.log ∘ ρ) x = gradX a₀ x)
(hGauss : ∀ (x : X), divX E x = ρ x - ρ_ion)
(hDivLinear : ∀ (α : ℝ) (G : X → Fin 3 → ℝ) (x : X), divX (fun (y : X) => α • G y) x = α * divX G x)
(x : X)
:
Poisson-Boltzmann algebraic core: force balance + Gauss → PB equation. Proved by Aristotle (Harmonic).
Corollary 3: The electric field vanishes: E(x) = 0. Reference: cor:E_zero
With u∞ = 0 and ρ constant, ∇a = 0, so force balance gives 0 = -2c₀ E, and since c₀ ≠ 0, E = 0.
theorem
VML.continuous_attains_max
{X : Type u_1}
[TopologicalSpace X]
[CompactSpace X]
[Nonempty X]
(g : X → ℝ)
(hg : Continuous g)
:
∃ (x_max : X), ∀ (x : X), g x ≤ g x_max
On a compact topological space, a continuous real-valued function attains its maximum. (Extreme value theorem.)
theorem
VML.continuous_attains_min
{X : Type u_1}
[TopologicalSpace X]
[CompactSpace X]
[Nonempty X]
(g : X → ℝ)
(hg : Continuous g)
:
∃ (x_min : X), ∀ (x : X), g x_min ≤ g x
On a compact topological space, a continuous real-valued function attains its minimum. (Extreme value theorem.)
theorem
VML.poisson_boltzmann_from_vlasov
{X : Type u_1}
[FlatTorus3 X]
(f : X → (Fin 3 → ℝ) → ℝ)
(E B : X → Fin 3 → ℝ)
(Ψ : ℝ → ℝ)
(ν : ℝ)
(ρ : X → ℝ)
(ρ_ion : ℝ)
(_hf_pos : ∀ (x : X) (v : Fin 3 → ℝ), 0 < f x v)
(_hf_smooth : ∀ (x : X), ContDiff ℝ 3 (f x))
(_hf_int : ∀ (x : X), MeasureTheory.Integrable (f x) MeasureTheory.volume)
(_hΨ : ∀ (r : ℝ), 0 < Ψ r)
(_hρ_def : ∀ (x : X), ρ x = ∫ (v : Fin 3 → ℝ), f x v)
(_hGauss : ∀ (x : X), FlatTorus3.divX E x = ρ x - ρ_ion)
(_hDiff_fv : ∀ (v : Fin 3 → ℝ), FlatTorus3.IsSpatiallySmooth 2 fun (x : X) => f x v)
(_hVlasov :
∀ (x : X) (v : Fin 3 → ℝ),
v ⬝ᵥ FlatTorus3.gradX (fun (y : X) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator Ψ (f x) v)
(c₀ : ℝ)
: