The exterior cutoff calculation from compact-field flux #
The whole exterior lies outside every ball contained in the cell.
A genuine face belongs to the exterior of either incident open cell.
theorem
LiebThirring.norm_ge_on_voronoiExterior
{M : ℕ}
(R : Fin M → Position)
(k : Fin M)
(a : ℝ)
(hball : Metric.ball (R k) a ⊆ voronoiCell R k)
{x : Position}
(hx : x ∈ (voronoiCell R k)ᶜ)
:
The whole exterior lies outside every ball contained in the cell.
theorem
LiebThirring.voronoiFace_subset_exterior
{M : ℕ}
(R : Fin M → Position)
(hR : Function.Injective R)
{k l : Fin M}
(hkl : k ≠ l)
:
voronoiFace R k l ⊆ (voronoiCell R k)ᶜ
A genuine face belongs to the exterior of either incident open cell.
theorem
LiebThirring.inner_exteriorInverseSquareField_on_face
{M : ℕ}
(R : Fin M → Position)
(hR : Function.Injective R)
{k l : Fin M}
(hkl : k ≠ l)
{y : Position}
(hy : y ∈ voronoiFace R k l)
:
inner ℝ (bisectorNormal R k l) (exteriorInverseSquareField (R k) y) = -2 * (nuclearHalfDistance R k l / ‖y - R k‖ ^ 4)
Exact normal value of the inverse-square gradient on a bisector face.
theorem
LiebThirring.integrable_exteriorFluxCutoff_mul
(μ : MeasureTheory.Measure Position)
(c : Position)
(T : ℝ)
(f : Position → ℝ)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : Position) => exteriorFluxCutoff c T x * f x) μ
Integrability of a cutoff multiplied by any integrable density.
theorem
LiebThirring.integrable_exteriorFluxDefect_mul
(μ : MeasureTheory.Measure Position)
(c : Position)
(T : ℝ)
(f : Position → ℝ)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : Position) => exteriorFluxDefect (T⁻¹ • (x - c)) * f x) μ
Integrability of the derivative defect multiplied by any integrable density.
theorem
LiebThirring.integral_voronoiExterior_cutoff_of_compact_flux
{M : ℕ}
(R : Fin M → Position)
(hR : Function.Injective R)
(hM : 2 ≤ M)
(k : Fin M)
(hFlux :
∀ (V : Position → Position),
ContDiff ℝ 1 V →
HasCompactSupport V →
∫ (x : Position) in (voronoiCell R k)ᶜ, positionDivergence V x = -∑ l : { l : Fin M // l ≠ k },
∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯)
(T : ℝ)
(hT : 0 < T)
:
(∫ (x : Position) in (voronoiCell R k)ᶜ, exteriorFluxCutoff (R k) T x * (1 / ‖x - R k‖ ^ 4)) - ∫ (x : Position) in (voronoiCell R k)ᶜ, exteriorFluxDefect (T⁻¹ • (x - R k)) * (1 / ‖x - R k‖ ^ 4) = ∑ l : { l : Fin M // l ≠ k },
∫ (y : Position) in voronoiFace R k ↑l, exteriorFluxCutoff (R k) T y * (nuclearHalfDistance R k ↑l / ‖y - R k‖ ^ 4) ∂bisectorSurfaceMeasure R hR k ↑l ⋯
Exact truncated balance, conditional only on compact C¹ flux.
theorem
LiebThirring.integral_voronoiExterior_inverse_fourth_of_compact_flux
{M : ℕ}
(R : Fin M → Position)
(hR : Function.Injective R)
(hM : 2 ≤ M)
(k : Fin M)
(hFlux :
∀ (V : Position → Position),
ContDiff ℝ 1 V →
HasCompactSupport V →
∫ (x : Position) in (voronoiCell R k)ᶜ, positionDivergence V x = -∑ l : { l : Fin M // l ≠ k },
∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯)
:
The full real exterior identity after the proved cutoff passage from compact C¹ flux.
theorem
LiebThirring.lintegral_voronoiExterior_inverse_fourth_of_compact_flux
{M : ℕ}
(R : Fin M → Position)
(hR : Function.Injective R)
(hM : 2 ≤ M)
(k : Fin M)
(hFlux :
∀ (V : Position → Position),
ContDiff ℝ 1 V →
HasCompactSupport V →
∫ (x : Position) in (voronoiCell R k)ᶜ, positionDivergence V x = -∑ l : { l : Fin M // l ≠ k },
∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯)
:
The full extended nonnegative exterior identity from a compact C¹ flux identity.