The canonical particle and edge conventions

def HsVirial.hardSphereEdgeKey {k : ℕ} (e : Sym2 (Fin k)) : Lex (Fin k × Fin k)

The lexicographic key given by the smaller and larger endpoints of an edge.

Equations

• HsVirial.hardSphereEdgeKey e = toLex (e.inf, e.sup)

@[instance_reducible]

noncomputable def HsVirial.hardSphereEdgeLinearOrder (k : ℕ) : LinearOrder (Sym2 (Fin k))

Order unordered edges lexicographically by their sorted endpoints.

Equations

• HsVirial.hardSphereEdgeLinearOrder k = LinearOrder.lift' HsVirial.hardSphereEdgeKey ⋯

@[instance_reducible]

noncomputable instance HsVirial.hardSphereEdgeOrder (k : ℕ) : LinearOrder (Sym2 (Fin k))

Equations

• HsVirial.hardSphereEdgeOrder k = HsVirial.hardSphereEdgeLinearOrder k

@[reducible, inline]

abbrev HsVirial.HardSphereConfiguration (k d : ℕ) : Type

Positions of the free particles, with the distinguished particle anchored at zero.

Equations

• HsVirial.HardSphereConfiguration k d = (Fin (k - 1) → HsVirial.HSPosition d)

def HsVirial.hardSphereFreeIndex {k : ℕ} [NeZero k] (i : Fin k) (hi : i ≠ 0) : Fin (k - 1)

The zero-based coordinate index of a particle other than the anchored particle.

Equations

• HsVirial.hardSphereFreeIndex i hi = ⟨↑i - 1, ⋯⟩

def HsVirial.hardSphereFreeParticleIndex {k : ℕ} (i : Fin (k - 1)) : Fin k

The particle label corresponding to a free coordinate.

Equations

• HsVirial.hardSphereFreeParticleIndex i = ⟨↑i + 1, ⋯⟩

def HsVirial.hardSpherePosition {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (i : Fin k) : HSPosition d

Recover a particle position, assigning zero to the anchored particle.

Equations

• HsVirial.hardSpherePosition r i = if hi : i = 0 then 0 else r (HsVirial.hardSphereFreeIndex i hi)

@[simp]

theorem HsVirial.hardSpherePosition_zero {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) : hardSpherePosition r 0 = 0

@[simp]

theorem HsVirial.hardSpherePosition_free {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (i : Fin (k - 1)) : hardSpherePosition r (hardSphereFreeParticleIndex i) = r i

theorem HsVirial.continuous_hardSpherePosition {k d : ℕ} [NeZero k] (i : Fin k) : Continuous fun (x : HardSphereConfiguration k d) => hardSpherePosition x i

noncomputable def HsVirial.hardSphereActiveExact {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) : Sym2 (Fin k) → Bool

Record whether the two endpoint positions of an edge are less than one unit apart.

Equations

• HsVirial.hardSphereActiveExact r = Sym2.lift ⟨fun (i j : Fin k) => decide (‖HsVirial.hardSpherePosition r i - HsVirial.hardSpherePosition r j‖ < 1), ⋯⟩

@[simp]

theorem HsVirial.hardSphereActiveExact_mk {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (i j : Fin k) : hardSphereActiveExact r s(i, j) = decide (‖hardSpherePosition r i - hardSpherePosition r j‖ < 1)

theorem HsVirial.measurable_hardSphereActiveExact_edge {k d : ℕ} [NeZero k] (e : Sym2 (Fin k)) : Measurable fun (r : HardSphereConfiguration k d) => hardSphereActiveExact r e

theorem HsVirial.measurable_finite_bool_comp {X : Type u_1} {E : Type u_2} {Y : Type u_3} [MeasurableSpace X] [Finite E] [MeasurableSpace Y] (active : X → E → Bool) (hactive : ∀ (e : E), Measurable fun (x : X) => active x e) (g : (E → Bool) → Y) : Measurable fun (x : X) => g (active x)

theorem HsVirial.measurable_hardSphereOmega {k d : ℕ} [NeZero k] : Measurable fun (r : HardSphereConfiguration k d) => ↑(mayerKernel (hardSphereActiveExact r))

theorem HsVirial.measurable_hardSphereNBCRegion {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : MeasurableSet (nbcRegion hardSphereActiveExact T)

noncomputable def HsVirial.hardSphereEdgeDistance {V : Type u_1} {d : ℕ} (position : V → HSPosition d) (e : Sym2 V) : ℝ

The distance between the endpoints of an unordered edge.

Equations

• HsVirial.hardSphereEdgeDistance position e = Sym2.lift ⟨fun (i j : V) => ‖position i - position j‖, ⋯⟩ e

@[simp]

theorem HsVirial.hardSphereEdgeDistance_mk {V : Type u_1} {d : ℕ} (position : V → HSPosition d) (i j : V) : hardSphereEdgeDistance position s(i, j) = ‖position i - position j‖

theorem HsVirial.norm_sub_le_walk_length {V : Type u_1} {d : ℕ} {G : SimpleGraph V} {position : V → HSPosition d} {u v : V} (p : G.Walk u v) (hedge : ∀ e ∈ p.edges, hardSphereEdgeDistance position e < 1) : ‖position u - position v‖ ≤ ↑p.length

theorem HsVirial.hardSphereEdgeDistance_lt_one_of_overlap {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) {e : Sym2 (Fin k)} (he : e ∈ (overlapGraph (hardSphereActiveExact r)).edgeSet) : hardSphereEdgeDistance (hardSpherePosition r) e < 1

theorem HsVirial.hardSpherePosition_norm_lt_of_connected {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (hG : (overlapGraph (hardSphereActiveExact r)).Connected) (i : Fin k) : ‖hardSpherePosition r i‖ < ↑k

theorem HsVirial.hardSphereConfiguration_mem_closedBall_of_connected {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (hG : (overlapGraph (hardSphereActiveExact r)).Connected) : r ∈ Metric.closedBall 0 ↑k

theorem HsVirial.hardSphereMayerKernel_zero_of_not_connected {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) (hG : ¬(overlapGraph (hardSphereActiveExact r)).Connected) : mayerKernel (hardSphereActiveExact r) = 0

noncomputable def HsVirial.hardSphereOmega {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) : ℝ

The signed Mayer graph sum evaluated at the configuration's overlap graph.

Equations

• HsVirial.hardSphereOmega r = ↑(HsVirial.mayerKernel (HsVirial.hardSphereActiveExact r))

noncomputable def HsVirial.hardSphereBk {k d : ℕ} [NeZero k] : ℝ

The hard-sphere cluster integral normalized by the factorial of the particle count.

Equations

• HsVirial.hardSphereBk = (↑k.factorial)⁻¹ * ∫ (r : HsVirial.HardSphereConfiguration k d), HsVirial.hardSphereOmega r

noncomputable def HsVirial.hardSphereNBCVolume {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : ℝ

The volume of configurations assigned to a fixed no-broken-circuit tree.

Equations

• HsVirial.hardSphereNBCVolume T = MeasureTheory.volume.real (HsVirial.nbcRegion HsVirial.hardSphereActiveExact T)

theorem HsVirial.hardSphereConfiguration_mem_closedBall_of_region {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) {T : Finset (Sym2 (Fin k))} (hr : r ∈ nbcRegion hardSphereActiveExact T) : r ∈ Metric.closedBall 0 ↑k

theorem HsVirial.hardSphereOmega_zero_of_not_mem_closedBall {k d : ℕ} [NeZero k] {r : HardSphereConfiguration k d} (hr : r ∉ Metric.closedBall 0 ↑k) : hardSphereOmega r = 0

theorem HsVirial.hardSphereNBCRegion_measure_ne_top {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : MeasureTheory.volume (nbcRegion hardSphereActiveExact T) ≠ ⊤

theorem HsVirial.norm_bond_le_one {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) (e : Sym2 V) : ‖↑(bond x e)‖ ≤ 1

theorem HsVirial.norm_mayerKernel_real_le_card {V : Type u_1} [Fintype V] [DecidableEq V] (x : Sym2 V → Bool) : ‖↑(mayerKernel x)‖ ≤ ↑completeConnectedEdgeSubsets.card

theorem HsVirial.integrable_hardSphereOmega {k d : ℕ} [NeZero k] : MeasureTheory.Integrable hardSphereOmega MeasureTheory.volume

theorem HsVirial.integrable_hardSphereNBC_indicator {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : MeasureTheory.Integrable ((nbcRegion hardSphereActiveExact T).indicator fun (x : HardSphereConfiguration k d) => 1) MeasureTheory.volume

theorem HsVirial.real_abs_mayerKernel_eq_intMagnitude {V : Type u_1} [Fintype V] [DecidableEq V] (x : Sym2 V → Bool) : |↑(mayerKernel x)| = ↑(mayerKernel x).natAbs

theorem HsVirial.hardSphere_absOmega_eq_region_indicator_sum {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) : |hardSphereOmega r| = ∑ T ∈ treeUniverse, (nbcRegion hardSphereActiveExact T).indicator (fun (x : HardSphereConfiguration k d) => 1) r

theorem HsVirial.hardSphereOmega_eq_sign_mul_abs {k d : ℕ} [NeZero k] (r : HardSphereConfiguration k d) : hardSphereOmega r = (-1) ^ (k - 1) * |hardSphereOmega r|

theorem HsVirial.integral_abs_hardSphereOmega_eq_sum_volume {k d : ℕ} [NeZero k] : ∫ (r : HardSphereConfiguration k d), |hardSphereOmega r| = ∑ T ∈ treeUniverse, MeasureTheory.volume.real (nbcRegion hardSphereActiveExact T)

theorem HsVirial.integral_hardSphereOmega_eq_sign_mul_abs {k d : ℕ} [NeZero k] : ∫ (r : HardSphereConfiguration k d), hardSphereOmega r = (-1) ^ (k - 1) * ∫ (r : HardSphereConfiguration k d), |hardSphereOmega r|

theorem HsVirial.abs_integral_hardSphereOmega_eq_integral_abs {k d : ℕ} [NeZero k] : |∫ (r : HardSphereConfiguration k d), hardSphereOmega r| = ∫ (r : HardSphereConfiguration k d), |hardSphereOmega r|

theorem HsVirial.hardSphere_nbc_volume_identity_of_neZero {k d : ℕ} [NeZero k] (_hk : 2 ≤ k) : ↑k.factorial * |hardSphereBk| = ∑ T ∈ treeUniverse, hardSphereNBCVolume T

theorem HsVirial.hardSphere_nbc_volume_identity {k d : ℕ} (hk : 2 ≤ k) : have x := ⋯; ↑k.factorial * |hardSphereBk| = ∑ T ∈ treeUniverse, hardSphereNBCVolume T