HardSphereForkPackingCoordinates

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

theorem HsVirial.hardSphereReindexedBlockCoordinateEquiv_fst_apply {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) (x : Fin n → HSPosition 3) (i : Fin m) : (((hardSphereReindexedBlockCoordinateEquiv e) x).1 i).1 = x (e (Fin.castAdd q (finProdFinEquiv (i, 0))))

theorem HsVirial.hardSphereReindexedBlockCoordinateEquiv_snd_apply {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) (x : Fin n → HSPosition 3) (i : Fin m) : (((hardSphereReindexedBlockCoordinateEquiv e) x).1 i).2 = x (e (Fin.castAdd q (finProdFinEquiv (i, 1))))

theorem HsVirial.hardSphereBlockCoordinateEquiv_fst_apply (m q : ℕ) (x : Fin (m * 2 + q) → HSPosition 3) (i : Fin m) : (((hardSphereBlockCoordinateEquiv m q) x).1 i).1 = x (Fin.castAdd q (finProdFinEquiv (i, 0)))

theorem HsVirial.hardSphereBlockCoordinateEquiv_snd_apply (m q : ℕ) (x : Fin (m * 2 + q) → HSPosition 3) (i : Fin m) : (((hardSphereBlockCoordinateEquiv m q) x).1 i).2 = x (Fin.castAdd q (finProdFinEquiv (i, 1)))

theorem HsVirial.hardSphereBlockCoordinateEquiv_complement_apply (m q : ℕ) (x : Fin (m * 2 + q) → HSPosition 3) (i : Fin q) : ((hardSphereBlockCoordinateEquiv m q) x).2 i = x (Fin.natAdd (m * 2) i)

theorem HsVirial.hardSphereReindexedBlockCoordinateEquiv_symm_apply {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) (x : Fin n → HSPosition 3) (i : Fin (m * 2 + q)) : (hardSphereBlockCoordinateEquiv m q).symm ((hardSphereReindexedBlockCoordinateEquiv e) x) i = x (e i)

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

The rooted tree-difference coordinate carrying a fixed tree edge.

Equations

• HsVirial.hardSphereTreeEdgeIndex hT e he = ⋯.choose

theorem HsVirial.hardSphereTreeParentEdge_hardSphereTreeEdgeIndex {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (e : Sym2 (Fin k)) (he : e ∈ T) : hardSphereTreeParentEdge hT (hardSphereTreeEdgeIndex hT e he) = e

def HsVirial.hardSphereForkMemberVertex {k : ℕ} (f : HardSphereForkTriple k) (j : Fin 2) : Fin k

The two tree edges used by an order-compatible fork.

Equations

• HsVirial.hardSphereForkMemberVertex f j = if j = 0 then f.2.1 else f.2.2

def HsVirial.hardSphereForkMemberEdge {k : ℕ} (f : HardSphereForkTriple k) (j : Fin 2) : Sym2 (Fin k)

Choose one of the two center-to-leaf edges of a fork.

Equations

• HsVirial.hardSphereForkMemberEdge f j = if j = 0 then s(f.1, f.2.1) else s(f.1, f.2.2)

theorem HsVirial.hardSphereForkMemberEdge_eq {k : ℕ} (f : HardSphereForkTriple k) (j : Fin 2) : hardSphereForkMemberEdge f j = s(f.1, hardSphereForkMemberVertex f j)

theorem HsVirial.hardSphereForkMemberEdge_mem {k : ℕ} {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hP : hardSphereForkPacking T P) {f : HardSphereForkTriple k} (hf : f ∈ P) (j : Fin 2) : hardSphereForkMemberEdge f j ∈ T

noncomputable def HsVirial.hardSphereForkMemberIndex {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (f : HardSphereForkTriple k) (j : Fin 2) (he : hardSphereForkMemberEdge f j ∈ T) : Fin (k - 1)

The tree-difference coordinate corresponding to a fork edge.

Equations

• HsVirial.hardSphereForkMemberIndex hT f j he = HsVirial.hardSphereTreeEdgeIndex hT (HsVirial.hardSphereForkMemberEdge f j) he

theorem HsVirial.hardSphereTreeParentEdge_hardSphereForkMemberIndex {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (f : HardSphereForkTriple k) (j : Fin 2) (he : hardSphereForkMemberEdge f j ∈ T) : hardSphereTreeParentEdge hT (hardSphereForkMemberIndex hT f j he) = hardSphereForkMemberEdge f j

noncomputable def HsVirial.hardSphereForkMemberReversed {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (f : HardSphereForkTriple k) (j : Fin 2) (he : hardSphereForkMemberEdge f j ∈ T) : Bool

Whether the tree orientation of a fork edge opposes its center-to-leaf orientation.

Equations

• HsVirial.hardSphereForkMemberReversed hT f j he = decide (HsVirial.hardSphereTreeParent hT (HsVirial.hardSphereForkMemberIndex hT f j he) ≠ f.1)

theorem HsVirial.hardSphereForkMember_oriented_difference {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) {f : HardSphereForkTriple k} (hf : f ∈ P) (j : Fin 2) (he : hardSphereForkMemberEdge f j ∈ T) (r : HardSphereConfiguration k 3) : (if hardSphereForkMemberReversed hT f j he = true then -hardSphereTreeDifference hT r (hardSphereForkMemberIndex hT f j he) else hardSphereTreeDifference hT r (hardSphereForkMemberIndex hT f j he)) = hardSpherePosition r (hardSphereForkMemberVertex f j) - hardSpherePosition r f.1

noncomputable def HsVirial.hardSphereForkPackingMemberIndex {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : ↥P × Fin 2 → Fin (k - 1)

Assign tree-difference coordinates to the two members of each packed fork.

Equations

• HsVirial.hardSphereForkPackingMemberIndex hT hP z = HsVirial.hardSphereForkMemberIndex hT (↑z.1) z.2 ⋯

theorem HsVirial.hardSphereForkPackingMemberIndex_injective {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) : Function.Injective (hardSphereForkPackingMemberIndex hT hP)

noncomputable def HsVirial.hardSphereForkPackingMemberIndexFin {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : Fin P.card × Fin 2 → Fin (k - 1)

Index packed fork members using the finite enumeration of the packing.

Equations

• HsVirial.hardSphereForkPackingMemberIndexFin hT hP z = HsVirial.hardSphereForkPackingMemberIndex hT hP (P.equivFin.symm z.1, z.2)

noncomputable def HsVirial.hardSphereForkPackingMemberReversed {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin P.card) (j : Fin 2) : Bool

The orientation correction for an enumerated packed fork edge.

Equations

• HsVirial.hardSphereForkPackingMemberReversed hT hP i j = HsVirial.hardSphereForkMemberReversed hT (↑(P.equivFin.symm i)) j ⋯

theorem HsVirial.hardSphereForkPackingMember_oriented_difference {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) (i : Fin P.card) (j : Fin 2) (r : HardSphereConfiguration k 3) : (if hardSphereForkPackingMemberReversed hT hP i j = true then -hardSphereTreeDifference hT r (hardSphereForkPackingMemberIndexFin hT hP (i, j)) else hardSphereTreeDifference hT r (hardSphereForkPackingMemberIndexFin hT hP (i, j))) = hardSpherePosition r (hardSphereForkMemberVertex (↑(P.equivFin.symm i)) j) - hardSpherePosition r (↑(P.equivFin.symm i)).1

theorem HsVirial.hardSphereForkPackingMemberIndexFin_injective {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) : Function.Injective (hardSphereForkPackingMemberIndexFin hT hP)

noncomputable def HsVirial.hardSphereForkPackingFlatMemberIndex {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : Fin (P.card * 2) → Fin (k - 1)

Flatten the two coordinate indices per packed fork into one finite index.

Equations

• HsVirial.hardSphereForkPackingFlatMemberIndex hT hP z = HsVirial.hardSphereForkPackingMemberIndexFin hT hP (finProdFinEquiv.symm z)

theorem HsVirial.hardSphereForkPackingFlatMemberIndex_injective {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) : Function.Injective (hardSphereForkPackingFlatMemberIndex hT hP)

noncomputable def HsVirial.hardSphereForkPackingSelectedIndices {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : Finset (Fin (k - 1))

The set of tree coordinates used by the fork packing.

Equations

• HsVirial.hardSphereForkPackingSelectedIndices hT hP = Finset.image (HsVirial.hardSphereForkPackingFlatMemberIndex hT hP) Finset.univ

theorem HsVirial.hardSphereForkPackingSelectedIndices_card {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) : (hardSphereForkPackingSelectedIndices hT hP).card = P.card * 2

noncomputable def HsVirial.hardSphereForkPackingSelectedEquiv {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : Fin (P.card * 2) ≃ ↥(hardSphereForkPackingSelectedIndices hT hP)

The bijection from packed edge indices to their selected tree coordinates.

Equations

• HsVirial.hardSphereForkPackingSelectedEquiv hT hP = Equiv.ofBijective (fun (i : Fin (P.card * 2)) => ⟨HsVirial.hardSphereForkPackingFlatMemberIndex hT hP i, ⋯⟩) ⋯

noncomputable def HsVirial.hardSphereForkPackingComplementCard {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : ℕ

The number of tree coordinates not used by the fork packing.

Equations

• HsVirial.hardSphereForkPackingComplementCard hT hP = Fintype.card { i : Fin (k - 1) // i ∉ HsVirial.hardSphereForkPackingSelectedIndices hT hP }

theorem HsVirial.hardSphereForkPackingComplementCard_eq {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} {hT : T ∈ treeUniverse} (hP : hardSphereForkPacking T P) : hardSphereForkPackingComplementCard hT hP = k - 1 - P.card * 2

noncomputable def HsVirial.hardSphereForkPackingIndexEquiv {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : Fin (P.card * 2 + hardSphereForkPackingComplementCard hT hP) ≃ Fin (k - 1)

Reindex tree coordinates with packed fork edges first and unused edges last.

Equations

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

theorem HsVirial.hardSphereForkPackingIndexEquiv_member {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin P.card) (j : Fin 2) : (hardSphereForkPackingIndexEquiv hT hP) (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, j))) = hardSphereForkPackingMemberIndexFin hT hP (i, j)

theorem HsVirial.hardSphereForkPackingIndexEquiv_selected_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin (P.card * 2)) : (hardSphereForkPackingIndexEquiv hT hP) (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) i) = hardSphereForkPackingFlatMemberIndex hT hP i

theorem HsVirial.hardSphereForkPackingIndexEquiv_complement_not_mem {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin (hardSphereForkPackingComplementCard hT hP)) : (hardSphereForkPackingIndexEquiv hT hP) (Fin.natAdd (P.card * 2) i) ∉ hardSphereForkPackingSelectedIndices hT hP

noncomputable def HsVirial.hardSphereForkPackingRawBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : HardSphereConfiguration k 3 → (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)

Group tree-difference coordinates into packed pairs and remaining single coordinates.

Equations

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

theorem HsVirial.measurePreserving_hardSphereForkPackingRawBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : MeasureTheory.MeasurePreserving (hardSphereForkPackingRawBlockMap hT hP) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereForkPackingRawBlockMap_flat_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (r : HardSphereConfiguration k 3) (i : Fin (P.card * 2 + hardSphereForkPackingComplementCard hT hP)) : (hardSphereBlockCoordinateEquiv P.card (hardSphereForkPackingComplementCard hT hP)).symm (hardSphereForkPackingRawBlockMap hT hP r) i = hardSphereTreeDifferencePositionMap hT r ((hardSphereForkPackingIndexEquiv hT hP) i)

def HsVirial.hardSphereApplyReversal (reverse : Bool) (x : HSPosition 3) : HSPosition 3

Negate a position exactly when the orientation flag requests reversal.

Equations

• HsVirial.hardSphereApplyReversal reverse x = if reverse = true then -x else x

theorem HsVirial.measurePreserving_hardSphereApplyReversal (reverse : Bool) : MeasureTheory.MeasurePreserving (hardSphereApplyReversal reverse) MeasureTheory.volume MeasureTheory.volume

noncomputable def HsVirial.hardSphereForkPackingFlatReversed {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin (P.card * 2 + hardSphereForkPackingComplementCard hT hP)) : Bool

The orientation reversal flag for a flattened packed coordinate.

Equations

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

noncomputable def HsVirial.hardSphereForkPackingFlatSignMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : (Fin (P.card * 2 + hardSphereForkPackingComplementCard hT hP) → HSPosition 3) → Fin (P.card * 2 + hardSphereForkPackingComplementCard hT hP) → HSPosition 3

Apply all orientation corrections to the flattened tree coordinates.

Equations

• HsVirial.hardSphereForkPackingFlatSignMap hT hP x i = HsVirial.hardSphereApplyReversal (HsVirial.hardSphereForkPackingFlatReversed hT hP i) (x i)

theorem HsVirial.hardSphereForkPackingFlatReversed_member {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin P.card) (j : Fin 2) : hardSphereForkPackingFlatReversed hT hP (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, j))) = hardSphereForkPackingMemberReversed hT hP i j

theorem HsVirial.hardSphereForkPackingFlatReversed_complement {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (i : Fin (hardSphereForkPackingComplementCard hT hP)) : hardSphereForkPackingFlatReversed hT hP (Fin.natAdd (P.card * 2) i) = false

theorem HsVirial.measurePreserving_hardSphereForkPackingFlatSignMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : MeasureTheory.MeasurePreserving (hardSphereForkPackingFlatSignMap hT hP) MeasureTheory.volume MeasureTheory.volume

noncomputable def HsVirial.hardSphereForkPackingSignedBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3) → (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)

Group the orientation-corrected coordinates into fork pairs and single positions.

Equations

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

theorem HsVirial.measurePreserving_hardSphereForkPackingSignedBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : MeasureTheory.MeasurePreserving (hardSphereForkPackingSignedBlockMap hT hP) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereForkPackingSignedBlockMap_fst_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (z : (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)) (i : Fin P.card) : ((hardSphereForkPackingSignedBlockMap hT hP z).1 i).1 = hardSphereApplyReversal (hardSphereForkPackingFlatReversed hT hP (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, 0)))) ((hardSphereBlockCoordinateEquiv P.card (hardSphereForkPackingComplementCard hT hP)).symm z (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, 0))))

theorem HsVirial.hardSphereForkPackingSignedBlockMap_snd_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (z : (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)) (i : Fin P.card) : ((hardSphereForkPackingSignedBlockMap hT hP z).1 i).2 = hardSphereApplyReversal (hardSphereForkPackingFlatReversed hT hP (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, 1)))) ((hardSphereBlockCoordinateEquiv P.card (hardSphereForkPackingComplementCard hT hP)).symm z (Fin.castAdd (hardSphereForkPackingComplementCard hT hP) (finProdFinEquiv (i, 1))))

theorem HsVirial.hardSphereForkPackingSignedBlockMap_complement_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (z : (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)) (i : Fin (hardSphereForkPackingComplementCard hT hP)) : (hardSphereForkPackingSignedBlockMap hT hP z).2 i = hardSphereApplyReversal (hardSphereForkPackingFlatReversed hT hP (Fin.natAdd (P.card * 2) i)) ((hardSphereBlockCoordinateEquiv P.card (hardSphereForkPackingComplementCard hT hP)).symm z (Fin.natAdd (P.card * 2) i))

noncomputable def HsVirial.hardSphereForkPackingBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : HardSphereConfiguration k 3 → (Fin P.card → HSPosition 3 × HSPosition 3) × (Fin (hardSphereForkPackingComplementCard hT hP) → HSPosition 3)

The configuration-to-block map used for the simultaneous fork volume estimate.

Equations

• HsVirial.hardSphereForkPackingBlockMap hT hP = HsVirial.hardSphereForkPackingSignedBlockMap hT hP ∘ HsVirial.hardSphereForkPackingRawBlockMap hT hP

theorem HsVirial.hardSphereForkPackingBlockMap_fst_member_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (r : HardSphereConfiguration k 3) (i : Fin P.card) : ((hardSphereForkPackingBlockMap hT hP r).1 i).1 = hardSpherePosition r (hardSphereForkMemberVertex (↑(P.equivFin.symm i)) 0) - hardSpherePosition r (↑(P.equivFin.symm i)).1

theorem HsVirial.hardSphereForkPackingBlockMap_snd_member_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (r : HardSphereConfiguration k 3) (i : Fin P.card) : ((hardSphereForkPackingBlockMap hT hP r).1 i).2 = hardSpherePosition r (hardSphereForkMemberVertex (↑(P.equivFin.symm i)) 1) - hardSpherePosition r (↑(P.equivFin.symm i)).1

theorem HsVirial.hardSphereForkPackingBlockMap_complement_apply {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) (r : HardSphereConfiguration k 3) (i : Fin (hardSphereForkPackingComplementCard hT hP)) : (hardSphereForkPackingBlockMap hT hP r).2 i = hardSphereTreeDifferencePositionMap hT r ((hardSphereForkPackingIndexEquiv hT hP) (Fin.natAdd (P.card * 2) i))

theorem HsVirial.hardSphereForkPackingBlockMap_mem_separatedBlockProductRegion {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) {r : HardSphereConfiguration k 3} (hr : r ∈ hardSphereTreeRegion T) (hrAvoid : r ∈ hardSphereForkAvoidanceRegion T P) : hardSphereForkPackingBlockMap hT hP r ∈ hardSphereSeparatedBlockProductRegion P.card (hardSphereForkPackingComplementCard hT hP)

theorem HsVirial.measurePreserving_hardSphereForkPackingBlockMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : MeasureTheory.MeasurePreserving (hardSphereForkPackingBlockMap hT hP) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphere_nbc_region_real_volume_le_of_forkPacking {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HardSphereForkTriple k)} (hT : T ∈ treeUniverse) (hP : hardSphereForkPacking T P) : MeasureTheory.volume.real (nbcRegion hardSphereActiveExact T) ≤ MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ P.card * hardSphereKappa ^ hardSphereForkPackingComplementCard hT hP

theorem HsVirial.hardSphereNBCRegion_real_volume_le_forkFactor {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.volume.real (nbcRegion hardSphereActiveExact T) ≤ (17 / 32) ^ hardSphereNu T * hardSphereKappa ^ (k - 1)