Concrete tree and fork regions

def HsVirial.hardSphereFork {k : ℕ} (T : Finset (Sym2 (Fin k))) (a b c : Fin k) : Prop

An order-compatible fork (a,b,c) with a < b < c; a is its center and b,c are its two leaves.

Equations

• HsVirial.hardSphereFork T a b c = (a < b ∧ b < c ∧ s(a, b) ∈ T ∧ s(a, c) ∈ T)

theorem HsVirial.hardSphereEdgeLE_fork_chord {k : ℕ} {a b c : Fin k} (hab : a < b) (hbc : b < c) : graphEdgeLE s(a, b) s(b, c)

theorem HsVirial.hardSphereEdgeLE_fork_member {k : ℕ} {a b c : Fin k} (hab : a < b) (hbc : b < c) : graphEdgeLE s(a, c) s(b, c)

theorem HsVirial.isGraphForest_of_card_le_two {V : Type u_1} [Fintype V] {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : A ⊆ graphEdgeFinset G) (hcard : A.card ≤ 2) : IsGraphForest G A

theorem HsVirial.isGraphTriangleCircuit {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {a b c : V} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (habG : s(a, b) ∈ G.edgeSet) (hacG : s(a, c) ∈ G.edgeSet) (hbcG : s(b, c) ∈ G.edgeSet) : IsGraphCircuit G {s(a, b), s(a, c), s(b, c)}

theorem HsVirial.hardSphere_nbc_region_excludes_fork_chord {k : ℕ} [NeZero k] (r : HardSphereConfiguration k 3) {T : Finset (Sym2 (Fin k))} {a b c : Fin k} (hr : r ∈ nbcRegion hardSphereActiveExact T) (hf : hardSphereFork T a b c) (hbc : ‖hardSpherePosition r b - hardSpherePosition r c‖ < 1) : False

noncomputable def HsVirial.hardSphereKappa : ℝ

The volume of the open unit ball in the three-dimensional position space.

Equations

• HsVirial.hardSphereKappa = MeasureTheory.volume.real (Metric.ball 0 1)

theorem HsVirial.hardSphereKappa_eq : hardSphereKappa = 4 * Real.pi / 3

def HsVirial.hardSphereTreeRegion {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : Set (HardSphereConfiguration k 3)

The hard-sphere configuration region owned by a fixed edge set.

Equations

• HsVirial.hardSphereTreeRegion T = {r : HsVirial.HardSphereConfiguration k 3 | ∀ e ∈ T, HsVirial.hardSphereActiveExact r e = true}

def HsVirial.hardSphereForkEvent {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) (_a b c : Fin k) : Set (HardSphereConfiguration k 3)

The part of a tree region where the two leaves of an order-compatible fork are also within range.

Equations

• HsVirial.hardSphereForkEvent T _a b c = HsVirial.hardSphereTreeRegion T ∩ {r : HsVirial.HardSphereConfiguration k 3 | ‖HsVirial.hardSpherePosition r b - HsVirial.hardSpherePosition r c‖ < 1}

theorem HsVirial.measurableSet_hardSphereTreeRegion {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : MeasurableSet (hardSphereTreeRegion T)

theorem HsVirial.measurableSet_hardSphereForkEvent {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) (a b c : Fin k) : MeasurableSet (hardSphereForkEvent T a b c)

theorem HsVirial.hardSphere_nbc_region_subset_tree_region {k : ℕ} [NeZero k] {r : HardSphereConfiguration k 3} {T : Finset (Sym2 (Fin k))} (hr : r ∈ nbcRegion hardSphereActiveExact T) : r ∈ hardSphereTreeRegion T

theorem HsVirial.hardSphere_forkEvent_subset_treeRegion {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {a b c : Fin k} : hardSphereForkEvent T a b c ⊆ hardSphereTreeRegion T

theorem HsVirial.hardSphere_nbc_region_disjoint_forkEvent {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {a b c : Fin k} (hf : hardSphereFork T a b c) : Disjoint (nbcRegion hardSphereActiveExact T) (hardSphereForkEvent T a b c)