HardSphereCompound

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

@[reducible, inline]

abbrev HsVirial.HardSphereForkTriple (k : ℕ) : Type

An ordered triple used to name an order-compatible fork (a,b,c) with a < b < c, where a is the center and b,c are the leaves.

Equations

• HsVirial.HardSphereForkTriple k = (Fin k × Fin k × Fin k)

def HsVirial.hardSphereForkSupport {k : ℕ} (f : HardSphereForkTriple k) : Finset (Fin k)

The three vertices supporting an order-compatible fork triple.

Equations

• HsVirial.hardSphereForkSupport f = {f.1, f.2.1, f.2.2}

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

The event associated with an order-compatible fork triple.

Equations

• HsVirial.hardSphereForkEventOfTriple T f = HsVirial.hardSphereForkEvent T f.1 f.2.1 f.2.2

def HsVirial.hardSphereForkPacking {k : ℕ} (T : Finset (Sym2 (Fin k))) (P : Finset (HardSphereForkTriple k)) : Prop

A finite family of pairwise vertex-disjoint, order-compatible forks in a tree.

Equations

• One or more equations did not get rendered due to their size.

theorem HsVirial.hardSphereForkSupport_card_of_mem_forkPacking {k : ℕ} {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) {f : HardSphereForkTriple k} (hf : f ∈ P) : (hardSphereForkSupport f).card = 3

theorem HsVirial.hardSphereForkPacking_three_mul_card_le {k : ℕ} {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : 3 * P.card ≤ k

theorem HsVirial.hardSphereForkPacking_two_mul_card_le_pred {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : 2 * P.card ≤ k - 1

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

The finite region avoiding every order-compatible fork event in a selected packing.

Equations

• HsVirial.hardSphereForkAvoidanceRegion T P = ⋂ f ∈ P, (HsVirial.hardSphereForkEventOfTriple T f)ᶜ

theorem HsVirial.measurableSet_hardSphereForkAvoidanceRegion {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) (P : Finset (HardSphereForkTriple k)) : MeasurableSet (hardSphereForkAvoidanceRegion T P)

theorem HsVirial.hardSphere_nbc_region_subset_forkAvoidance {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : nbcRegion hardSphereActiveExact T ⊆ hardSphereForkAvoidanceRegion T P

theorem HsVirial.hardSphere_nbc_region_measure_le_forkAvoidance {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : MeasureTheory.volume (nbcRegion hardSphereActiveExact T) ≤ MeasureTheory.volume (hardSphereForkAvoidanceRegion T P)

theorem HsVirial.hardSphere_treeRegion_mem_separatedPair_of_not_forkEvent {k : ℕ} [NeZero k] {r : HardSphereConfiguration k 3} {T : Finset (Sym2 (Fin k))} {a b c : Fin k} (hr : r ∈ hardSphereTreeRegion T) (hf : hardSphereFork T a b c) (havoid : r ∉ hardSphereForkEvent T a b c) : hardSphereForkRelativePair r a b c ∈ hardSphereSeparatedPairRegion

theorem HsVirial.hardSphere_treeRegion_mem_separatedPair_of_mem_forkAvoidance {k : ℕ} [NeZero k] {r : HardSphereConfiguration k 3} {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) (hr : r ∈ hardSphereTreeRegion T) (hrAvoid : r ∈ hardSphereForkAvoidanceRegion T P) {f : HardSphereForkTriple k} (hf : f ∈ P) : hardSphereForkRelativePair r f.1 f.2.1 f.2.2 ∈ hardSphereSeparatedPairRegion

def HsVirial.hardSphereForkPackingSeparatedRegion {k : ℕ} [NeZero k] (P : Finset (HardSphereForkTriple k)) : Set (HardSphereConfiguration k 3)

The simultaneous separated-pair constraints associated with an order-compatible fork packing.

Equations

• One or more equations did not get rendered due to their size.

theorem HsVirial.measurableSet_hardSphereForkPackingSeparatedRegion {k : ℕ} [NeZero k] (P : Finset (HardSphereForkTriple k)) : MeasurableSet (hardSphereForkPackingSeparatedRegion P)

theorem HsVirial.hardSphere_nbc_region_subset_forkPackingSeparatedRegion {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : nbcRegion hardSphereActiveExact T ⊆ hardSphereForkPackingSeparatedRegion P

theorem HsVirial.hardSphere_nbc_region_real_volume_le_of_separatedBlockMap {k m q : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (φ : HardSphereConfiguration k 3 → (Fin m → HSPosition 3 × HSPosition 3) × (Fin q → HSPosition 3)) (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hsubset : nbcRegion hardSphereActiveExact T ⊆ φ ⁻¹' hardSphereSeparatedBlockProductRegion m q) : MeasureTheory.volume.real (nbcRegion hardSphereActiveExact T) ≤ MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ m * hardSphereKappa ^ q

noncomputable def HsVirial.hardSphereForkPackings {k : ℕ} (T : Finset (Sym2 (Fin k))) : Finset (Finset (HardSphereForkTriple k))

All finite order-compatible fork packings of a fixed tree.

Equations

• HsVirial.hardSphereForkPackings T = Finset.filter (HsVirial.hardSphereForkPacking T) Finset.univ.powerset

noncomputable def HsVirial.hardSphereNu {k : ℕ} (T : Finset (Sym2 (Fin k))) : ℕ

The maximum cardinality of a pairwise vertex-disjoint, order-compatible fork packing.

Equations

• HsVirial.hardSphereNu T = (HsVirial.hardSphereForkPackings T).sup Finset.card

theorem HsVirial.hardSphereForkPackings_nonempty {k : ℕ} (T : Finset (Sym2 (Fin k))) : (hardSphereForkPackings T).Nonempty

theorem HsVirial.hardSphereForkPacking_card_le_nu {k : ℕ} {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) : P.card ≤ hardSphereNu T

theorem HsVirial.hardSphere_exists_forkPacking_card_eq_nu {k : ℕ} (T : Finset (Sym2 (Fin k))) : ∃ (P : Finset (HardSphereForkTriple k)), hardSphereForkPacking T P ∧ P.card = hardSphereNu T