HardSphereGeometry

Graph, coordinate, and measure constructions for the hard-sphere NBC volume identity.

noncomputable def HsVirial.hardSphereLens (s : ℝ) : ℝ

The equal-unit-ball lens formula used by the two-member star block.

Equations

• HsVirial.hardSphereLens s = Real.pi * (4 + s) * (2 - s) ^ 2 / 12

theorem HsVirial.hardSphereLens_eq_polynomial (s : ℝ) : hardSphereLens s = Real.pi / 12 * (16 - 12 * s + s ^ 3)

theorem HsVirial.intervalIntegral_hardSphereLens_mul_sq : ∫ (s : ℝ) in 0..1, hardSphereLens s * s ^ 2 = 5 * Real.pi / 24

theorem HsVirial.hardSphereLens_radial_identity : 4 * Real.pi * ∫ (s : ℝ) in 0..1, (hardSphereKappa - hardSphereLens s) * s ^ 2 = 17 * Real.pi ^ 2 / 18

theorem HsVirial.hardSphereSeparatedVolume_ratio_identity : 17 / 32 * hardSphereKappa ^ 2 = 17 * Real.pi ^ 2 / 18

def HsVirial.hardSphereProductBallRegion (n : ℕ) : Set (Fin n → HSPosition 3)

Independent unit-ball constraints on a finite product of position spaces.

Equations

• HsVirial.hardSphereProductBallRegion n = {r : Fin n → HsVirial.HSPosition 3 | ∀ (i : Fin n), r i ∈ Metric.ball 0 1}

theorem HsVirial.measurableSet_hardSphereProductBallRegion (n : ℕ) : MeasurableSet (hardSphereProductBallRegion n)

theorem HsVirial.hardSphereProductBallRegion_volume (n : ℕ) : MeasureTheory.volume.real (hardSphereProductBallRegion n) = hardSphereKappa ^ n