Elementary tree-coordinate shears

def HsVirial.hardSphereTreeGraph {k : ℕ} (T : Finset (Sym2 (Fin k))) : SimpleGraph (Fin k)

The graph induced by a finite set of particle edges.

Equations

• HsVirial.hardSphereTreeGraph T = SimpleGraph.fromEdgeSet ↑T

theorem HsVirial.hardSphereTreeGraph_isTree {k : ℕ} {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : (hardSphereTreeGraph T).IsTree

theorem HsVirial.hardSphereTree_parent_exists {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : ∃ (p : Fin k), p ≠ hardSphereFreeParticleIndex i ∧ (hardSphereTreeGraph T).Adj p (hardSphereFreeParticleIndex i) ∧ (hardSphereTreeGraph T).dist 0 p + 1 = (hardSphereTreeGraph T).dist 0 (hardSphereFreeParticleIndex i)

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

The parent of a free particle in the tree rooted at the anchored particle.

Equations

• HsVirial.hardSphereTreeParent hT i = ⋯.choose

theorem HsVirial.hardSphereTreeParent_ne {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : hardSphereTreeParent hT i ≠ hardSphereFreeParticleIndex i

theorem HsVirial.hardSphereTreeParent_adj {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : (hardSphereTreeGraph T).Adj (hardSphereTreeParent hT i) (hardSphereFreeParticleIndex i)

theorem HsVirial.hardSphereTreeParent_dist_succ {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : (hardSphereTreeGraph T).dist 0 (hardSphereTreeParent hT i) + 1 = (hardSphereTreeGraph T).dist 0 (hardSphereFreeParticleIndex i)

theorem HsVirial.hardSphereTreeParent_mem {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) : s(hardSphereTreeParent hT i, hardSphereFreeParticleIndex i) ∈ T

theorem HsVirial.hardSphereFreeParticleIndex_freeIndex {k : ℕ} [NeZero k] (v : Fin k) (hv : v ≠ 0) : hardSphereFreeParticleIndex (hardSphereFreeIndex v hv) = v

@[instance_reducible]

noncomputable def HsVirial.hardSphereTreeIndexOrder {k : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) (_hT : T ∈ treeUniverse) : LinearOrder (Fin (k - 1))

An order of free particles compatible with their rooted-tree depth.

Equations

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

theorem HsVirial.hardSphereTreeParent_index_lt {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (i : Fin (k - 1)) (hp : hardSphereTreeParent hT i ≠ 0) : hardSphereFreeIndex (hardSphereTreeParent hT i) hp < i

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

The position difference along the rooted parent edge of a free particle.

Equations

• HsVirial.hardSphereTreeDifference hT r i = HsVirial.hardSpherePosition r (HsVirial.hardSphereFreeParticleIndex i) - HsVirial.hardSpherePosition r (HsVirial.hardSphereTreeParent hT i)

theorem HsVirial.hardSphereTreeDifference_eq_coordinate_sub {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (r : HardSphereConfiguration k 3) (i : Fin (k - 1)) : hardSphereTreeDifference hT r i = r i - hardSpherePosition r (hardSphereTreeParent hT i)

theorem HsVirial.hardSphereTreeDifference_norm_lt_one {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) {r : HardSphereConfiguration k 3} (hr : r ∈ hardSphereTreeRegion T) (i : Fin (k - 1)) : ‖hardSphereTreeDifference hT r i‖ < 1

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

The product of unit-ball constraints for all rooted tree differences.

Equations

• HsVirial.hardSphereTreeDifferenceRegion hT = {r : HsVirial.HardSphereConfiguration k 3 | ∀ (i : Fin (k - 1)), HsVirial.hardSphereTreeDifference hT r i ∈ Metric.ball 0 1}

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

theorem HsVirial.measurableSet_hardSphereTreeDifferenceRegion {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasurableSet (hardSphereTreeDifferenceRegion hT)

def HsVirial.hardSphereScalarShear {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent child : ι) (hpc : parent ≠ child) : (ι → ℝ) → ι → ℝ

Subtract the parent scalar coordinate from a child scalar coordinate.

Equations

• HsVirial.hardSphereScalarShear parent child hpc = ⇑(Matrix.toLin' { i := child, j := parent, hij := ⋯, c := -1 }.toMatrix)

theorem HsVirial.measurePreserving_hardSphereScalarShear {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent child : ι) (hpc : parent ≠ child) : MeasureTheory.MeasurePreserving (hardSphereScalarShear parent child hpc) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereScalarShear_apply_child {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent child : ι) (hpc : parent ≠ child) (x : ι → ℝ) : hardSphereScalarShear parent child hpc x child = x child - x parent

theorem HsVirial.hardSphereScalarShear_apply_parent {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent child : ι) (hpc : parent ≠ child) (x : ι → ℝ) : hardSphereScalarShear parent child hpc x parent = x parent

theorem HsVirial.hardSphereScalarShear_apply_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent child q : ι) (hpc : parent ≠ child) (hqc : q ≠ child) (x : ι → ℝ) : hardSphereScalarShear parent child hpc x q = x q