HardSphereTreeEdges

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

noncomputable def HsVirial.hardSphereTreeParentEdge {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : Sym2 (Fin k)

The tree edge selected by the rooted parent of a free vertex.

Equations

• HsVirial.hardSphereTreeParentEdge hT i = s(HsVirial.hardSphereTreeParent hT i, HsVirial.hardSphereFreeParticleIndex i)

theorem HsVirial.hardSphereTreeParentEdge_mem {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : hardSphereTreeParentEdge hT i ∈ T

theorem HsVirial.hardSphereTreeParentEdge_injective {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : Function.Injective (hardSphereTreeParentEdge hT)

noncomputable def HsVirial.hardSphereTreeParentEdgeFinset {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : Finset (Sym2 (Fin k))

The edges joining each free particle to its rooted-tree parent.

Equations

• HsVirial.hardSphereTreeParentEdgeFinset hT = Finset.image (HsVirial.hardSphereTreeParentEdge hT) Finset.univ

theorem HsVirial.hardSphereTreeParentEdgeFinset_subset {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : hardSphereTreeParentEdgeFinset hT ⊆ T

theorem HsVirial.hardSphereTreeParentEdgeFinset_card {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : (hardSphereTreeParentEdgeFinset hT).card = k - 1

theorem HsVirial.hardSphereTreeEdgeFinset_eq {k : ℕ} {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : graphEdgeFinset (hardSphereTreeGraph T) = T

theorem HsVirial.hardSphereTreeEdgeFinset_card {k : ℕ} {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : T.card = k - 1

theorem HsVirial.hardSphereTreeParentEdgeFinset_eq {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : hardSphereTreeParentEdgeFinset hT = T

theorem HsVirial.hardSphereTreeRegion_eq_flatDifferencePreimage {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : hardSphereTreeRegion T = (fun (r : HardSphereConfiguration k 3) => (hardSphereTreeFlatDifferenceLinearMap hT) ((hardSphereCoordinateEquiv k) r)) ⁻¹' hardSphereFlatProductBallRegion (k - 1)