The actual Voronoi volume and boundary cutoff limits

The principal exterior volume term converges on the actual exterior.

The radial derivative error tends to zero on the actual exterior.

theorem LiebThirring.tendsto_integral_cutoff_voronoiExterior {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : Filter.Tendsto (fun (T : ℝ) => ∫ (x : Position) in (voronoiCell R k)ᶜ, exteriorFluxCutoff (R k) T x * (1 / ‖x - R k‖ ^ 4)) Filter.atTop (nhds (∫ (x : Position) in (voronoiCell R k)ᶜ, 1 / ‖x - R k‖ ^ 4))

The principal exterior volume term converges on the actual exterior.

theorem LiebThirring.tendsto_integral_defect_voronoiExterior {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : Filter.Tendsto (fun (T : ℝ) => ∫ (x : Position) in (voronoiCell R k)ᶜ, exteriorFluxDefect (T⁻¹ • (x - R k)) * (1 / ‖x - R k‖ ^ 4)) Filter.atTop (nhds 0)

The radial derivative error tends to zero on the actual exterior.

theorem LiebThirring.tendsto_integral_cutoff_voronoiFace {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : Filter.Tendsto (fun (T : ℝ) => ∫ (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 hkl) Filter.atTop (nhds (∫ (y : Position) in voronoiFace R k l, nuclearHalfDistance R k l / ‖y - R k‖ ^ 4 ∂bisectorSurfaceMeasure R hR k l hkl))

Every actual boundary term converges, including on unbounded genuine faces.