Triangular difference maps

def HsVirial.hardSphereParentDifferenceLinearMap {ι : Type u_1} (parent : ι → Option ι) : (ι → ℝ) →ₗ[ℝ] ι → ℝ

Subtract each coordinate's parent coordinate, retaining root coordinates unchanged.

Equations

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

theorem HsVirial.hardSphereParentDifferenceLinearMap_apply {ι : Type u_1} (parent : ι → Option ι) (x : ι → ℝ) (i : ι) : (hardSphereParentDifferenceLinearMap parent) x i = match parent i with | none => x i | some p => x i - x p

theorem HsVirial.hardSphereParentDifferenceLinearMap_toMatrix_lower {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent : ι → Option ι) (ord : LinearOrder ι) (hlt : ∀ (i p : ι), parent i = some p → p < i) : (LinearMap.toMatrix' (hardSphereParentDifferenceLinearMap parent)).BlockTriangular ⇑OrderDual.toDual

theorem HsVirial.hardSphereParentDifferenceLinearMap_toMatrix_diag {ι : Type u_1} [Fintype ι] [DecidableEq ι] (parent : ι → Option ι) (ord : LinearOrder ι) (hlt : ∀ (i p : ι), parent i = some p → p < i) (i : ι) : LinearMap.toMatrix' (hardSphereParentDifferenceLinearMap parent) i i = 1

theorem HsVirial.hardSphereParentDifferenceLinearMap_det {ι : Type u_1} [Finite ι] (parent : ι → Option ι) (ord : LinearOrder ι) (hlt : ∀ (i p : ι), parent i = some p → p < i) : LinearMap.det (hardSphereParentDifferenceLinearMap parent) = 1

theorem HsVirial.measurePreserving_hardSphereParentDifferenceLinearMap {ι : Type u_1} [Fintype ι] (parent : ι → Option ι) (ord : LinearOrder ι) (hlt : ∀ (i p : ι), parent i = some p → p < i) : MeasureTheory.MeasurePreserving (⇑(hardSphereParentDifferenceLinearMap parent)) MeasureTheory.volume MeasureTheory.volume

Rooted tree coordinates

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

The parent's free index, or no index when the parent is the anchored particle.

Equations

• HsVirial.hardSphereTreeParentFreeIndex hT i = if hp : HsVirial.hardSphereTreeParent hT i = 0 then none else some (HsVirial.hardSphereFreeIndex (HsVirial.hardSphereTreeParent hT i) hp)

noncomputable def HsVirial.hardSphereTreeFlatParent {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (q : Fin (k - 1) × Fin 3) : Option (Fin (k - 1) × Fin 3)

Lift the particle-parent relation to each scalar spatial coordinate.

Equations

• HsVirial.hardSphereTreeFlatParent hT q = Option.map (fun (p : Fin (k - 1)) => (p, q.2)) (HsVirial.hardSphereTreeParentFreeIndex hT q.1)

@[instance_reducible]

noncomputable def HsVirial.hardSphereTreeFlatIndexOrder {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : LinearOrder (Fin (k - 1) × Fin 3)

Order flattened spatial coordinates compatibly with the rooted-tree order.

Equations

• HsVirial.hardSphereTreeFlatIndexOrder hT = LinearOrder.lift' (fun (q : Fin (k - 1) × Fin 3) => toLex (q.1, q.2)) ⋯

noncomputable def HsVirial.hardSphereTreeFlatDifferenceLinearMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : (Fin (k - 1) × Fin 3 → ℝ) →ₗ[ℝ] Fin (k - 1) × Fin 3 → ℝ

The linear transformation from scalar positions to scalar tree differences.

Equations

• HsVirial.hardSphereTreeFlatDifferenceLinearMap hT = HsVirial.hardSphereParentDifferenceLinearMap (HsVirial.hardSphereTreeFlatParent hT)

theorem HsVirial.hardSphereTreeFlatParent_lt {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (q p : Fin (k - 1) × Fin 3) : hardSphereTreeFlatParent hT q = some p → p < q

theorem HsVirial.measurePreserving_hardSphereTreeFlatDifferenceLinearMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.MeasurePreserving (⇑(hardSphereTreeFlatDifferenceLinearMap hT)) MeasureTheory.volume MeasureTheory.volume

Product-coordinate volume

def HsVirial.hardSphereCoordinateEquiv (k : ℕ) : HardSphereConfiguration k 3 ≃ᵐ (Fin (k - 1) × Fin 3 → ℝ)

Flatten an anchored three-dimensional configuration into scalar coordinates.

Equations

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

theorem HsVirial.measurePreserving_hardSphereCoordinateEquiv (k : ℕ) : MeasureTheory.MeasurePreserving (⇑(hardSphereCoordinateEquiv k)) MeasureTheory.volume MeasureTheory.volume

def HsVirial.hardSphereFlatProductBallRegion (n : ℕ) : Set (Fin n × Fin 3 → ℝ)

Flattened position arrays with every three-dimensional block in the unit ball.

Equations

• HsVirial.hardSphereFlatProductBallRegion n = {x : Fin n × Fin 3 → ℝ | ∀ (i : Fin n), ((MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) fun (a : Fin 3) => x (i, a)) ∈ Metric.ball 0 1}

theorem HsVirial.measurableSet_hardSphereFlatProductBallRegion (n : ℕ) : MeasurableSet (hardSphereFlatProductBallRegion n)

def HsVirial.hardSphereBlockBallRegion (n : ℕ) : Set (Fin n → Fin 3 → ℝ)

Arrays of three-coordinate blocks lying in the unit ball.

Equations

• HsVirial.hardSphereBlockBallRegion n = {x : Fin n → Fin 3 → ℝ | ∀ (i : Fin n), (MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) (x i) ∈ Metric.ball 0 1}

def HsVirial.hardSphereBlockToPositionEquiv (n : ℕ) : (Fin n → Fin 3 → ℝ) ≃ᵐ (Fin n → HSPosition 3)

Identify three-coordinate blocks with Euclidean positions, measurably.

Equations

• HsVirial.hardSphereBlockToPositionEquiv n = MeasurableEquiv.piCongrRight fun (x : Fin n) => MeasurableEquiv.toLp 2 (Fin 3 → ℝ)

theorem HsVirial.hardSphereBlockBallRegion_eq_preimage (n : ℕ) : hardSphereBlockBallRegion n = ⇑(hardSphereBlockToPositionEquiv n) ⁻¹' hardSphereProductBallRegion n

theorem HsVirial.measurableSet_hardSphereBlockBallRegion (n : ℕ) : MeasurableSet (hardSphereBlockBallRegion n)

theorem HsVirial.measurePreserving_hardSphereBlockToPositionEquiv (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(hardSphereBlockToPositionEquiv n)) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereFlatProductBallRegion_volume (n : ℕ) : MeasureTheory.volume.real (hardSphereFlatProductBallRegion n) = hardSphereKappa ^ n

The separated two-member block

def HsVirial.hardSphereSeparatedPairRegion : Set (HSPosition 3 × HSPosition 3)

Pairs of unit-ball positions separated by distance at least one.

Equations

• HsVirial.hardSphereSeparatedPairRegion = {p : HsVirial.HSPosition 3 × HsVirial.HSPosition 3 | p.1 ∈ Metric.ball 0 1 ∧ p.2 ∈ Metric.ball 0 1 ∧ 1 ≤ ‖p.1 - p.2‖}

theorem HsVirial.measurableSet_hardSphereSeparatedPairRegion : MeasurableSet hardSphereSeparatedPairRegion

Relative coordinates for a separated pair

def HsVirial.hardSpherePairCoordinateEquiv : HSPosition 3 × HSPosition 3 ≃ᵐ (Fin 2 × Fin 3 → ℝ)

Flatten a pair of three-dimensional Euclidean positions.

Equations

• HsVirial.hardSpherePairCoordinateEquiv = MeasurableEquiv.finTwoArrow.symm.trans (HsVirial.hardSphereCoordinateEquiv 3)

theorem HsVirial.measurePreserving_hardSpherePairCoordinateEquiv : MeasureTheory.MeasurePreserving (⇑hardSpherePairCoordinateEquiv) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSpherePairCoordinateEquiv_apply_zero (p : HSPosition 3 × HSPosition 3) (a : Fin 3) : hardSpherePairCoordinateEquiv p (0, a) = p.1.ofLp a

theorem HsVirial.hardSpherePairCoordinateEquiv_apply_one (p : HSPosition 3 × HSPosition 3) (a : Fin 3) : hardSpherePairCoordinateEquiv p (1, a) = p.2.ofLp a

theorem HsVirial.hardSpherePairCoordinate_block_zero (p : HSPosition 3 × HSPosition 3) : ((MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) fun (a : Fin 3) => hardSpherePairCoordinateEquiv p (0, a)) = p.1

theorem HsVirial.hardSpherePairCoordinate_block_one (p : HSPosition 3 × HSPosition 3) : ((MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) fun (a : Fin 3) => hardSpherePairCoordinateEquiv p (1, a)) = p.2

theorem HsVirial.hardSpherePairCoordinateEquiv_preimage_flatProductBallRegion : ⇑hardSpherePairCoordinateEquiv ⁻¹' hardSphereFlatProductBallRegion 2 = Metric.ball 0 1 ×ˢ Metric.ball 0 1

def HsVirial.hardSphereSeparatedPairFlatRegion : Set (Fin 2 × Fin 3 → ℝ)

The separated-pair region in flattened scalar coordinates.

Equations

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

theorem HsVirial.hardSpherePairCoordinateEquiv_image_separatedPairRegion : ⇑hardSpherePairCoordinateEquiv '' hardSphereSeparatedPairRegion = hardSphereSeparatedPairFlatRegion

theorem HsVirial.hardSphereSeparatedPairRegion_flatten_volume : MeasureTheory.volume.real (⇑hardSpherePairCoordinateEquiv '' hardSphereSeparatedPairRegion) = MeasureTheory.volume.real hardSphereSeparatedPairRegion

theorem HsVirial.hardSphereSeparatedPairRegion_flatten_volume_eq_flat : MeasureTheory.volume.real (⇑hardSpherePairCoordinateEquiv '' hardSphereSeparatedPairRegion) = MeasureTheory.volume.real hardSphereSeparatedPairFlatRegion

def HsVirial.hardSphereClosePairRegion : Set (HSPosition 3 × HSPosition 3)

Pairs of unit-ball positions separated by distance less than one.

Equations

• HsVirial.hardSphereClosePairRegion = {p : HsVirial.HSPosition 3 × HsVirial.HSPosition 3 | p.1 ∈ Metric.ball 0 1 ∧ p.2 ∈ Metric.ball 0 1 ∧ ‖p.1 - p.2‖ < 1}

theorem HsVirial.measurableSet_hardSphereClosePairRegion : MeasurableSet hardSphereClosePairRegion

theorem HsVirial.hardSphereSeparatedPairRegion_eq_product_sdiff_close : hardSphereSeparatedPairRegion = Metric.ball 0 1 ×ˢ Metric.ball 0 1 \ hardSphereClosePairRegion

theorem HsVirial.hardSphereClosePairRegion_subset_product : hardSphereClosePairRegion ⊆ Metric.ball 0 1 ×ˢ Metric.ball 0 1

theorem HsVirial.hardSphereSeparatedPairRegion_add_close_volume : MeasureTheory.volume hardSphereSeparatedPairRegion + MeasureTheory.volume hardSphereClosePairRegion = MeasureTheory.volume (Metric.ball 0 1 ×ˢ Metric.ball 0 1)

theorem HsVirial.hardSphereSeparatedPairRegion_real_add_close_volume : MeasureTheory.volume.real hardSphereSeparatedPairRegion + MeasureTheory.volume.real hardSphereClosePairRegion = hardSphereKappa ^ 2

def HsVirial.hardSpherePairParent (q : Fin 2 × Fin 3) : Option (Fin 2 × Fin 3)

The parent relation implementing the difference of the second position from the first.

Equations

• HsVirial.hardSpherePairParent q = if q.1 = 0 then none else some (0, q.2)

@[instance_reducible]

noncomputable def HsVirial.hardSpherePairIndexOrder : LinearOrder (Fin 2 × Fin 3)

The lexicographic order on particle and spatial indices for a pair.

Equations

• HsVirial.hardSpherePairIndexOrder = LinearOrder.lift' (fun (q : Fin 2 × Fin 3) => toLex (q.1, q.2)) HsVirial.hardSpherePairIndexOrder._proof_1

theorem HsVirial.hardSpherePairParent_lt (q p : Fin 2 × Fin 3) : hardSpherePairParent q = some p → p < q

def HsVirial.hardSpherePairDifferenceLinearMap : (Fin 2 × Fin 3 → ℝ) →ₗ[ℝ] Fin 2 × Fin 3 → ℝ

The linear parent-difference map on a flattened pair of positions.

Equations

• HsVirial.hardSpherePairDifferenceLinearMap = HsVirial.hardSphereParentDifferenceLinearMap HsVirial.hardSpherePairParent

theorem HsVirial.measurePreserving_hardSpherePairDifferenceLinearMap : MeasureTheory.MeasurePreserving (⇑hardSpherePairDifferenceLinearMap) MeasureTheory.volume MeasureTheory.volume

def HsVirial.hardSphereForkRelativePair {k : ℕ} [NeZero k] (r : HardSphereConfiguration k 3) (a b c : Fin k) : HSPosition 3 × HSPosition 3

The two leaf positions relative to the common center of a fork.

Equations

• HsVirial.hardSphereForkRelativePair r a b c = (HsVirial.hardSpherePosition r b - HsVirial.hardSpherePosition r a, HsVirial.hardSpherePosition r c - HsVirial.hardSpherePosition r a)

theorem HsVirial.hardSphere_nbc_region_mem_separatedPair {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) : hardSphereForkRelativePair r a b c ∈ hardSphereSeparatedPairRegion

def HsVirial.hardSphereSeparatedPairProductRegion (m : ℕ) : Set (Fin m → HSPosition 3 × HSPosition 3)

Families of separated pairs, each lying in the unit ball.

Equations

• HsVirial.hardSphereSeparatedPairProductRegion m = {x : Fin m → HsVirial.HSPosition 3 × HsVirial.HSPosition 3 | ∀ (i : Fin m), x i ∈ HsVirial.hardSphereSeparatedPairRegion}

theorem HsVirial.measurableSet_hardSphereSeparatedPairProductRegion (m : ℕ) : MeasurableSet (hardSphereSeparatedPairProductRegion m)

theorem HsVirial.hardSphereSeparatedPairProductRegion_volume (m : ℕ) : MeasureTheory.volume.real (hardSphereSeparatedPairProductRegion m) = MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ m

def HsVirial.hardSphereSeparatedBlockProductRegion (m q : ℕ) : Set ((Fin m → HSPosition 3 × HSPosition 3) × (Fin q → HSPosition 3))

A product of separated-pair regions and unconstrained unit-ball positions.

Equations

• HsVirial.hardSphereSeparatedBlockProductRegion m q = HsVirial.hardSphereSeparatedPairProductRegion m ×ˢ HsVirial.hardSphereProductBallRegion q

theorem HsVirial.measurableSet_hardSphereSeparatedBlockProductRegion (m q : ℕ) : MeasurableSet (hardSphereSeparatedBlockProductRegion m q)

theorem HsVirial.hardSphereSeparatedBlockProductRegion_volume (m q : ℕ) : MeasureTheory.volume.real (hardSphereSeparatedBlockProductRegion m q) = MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ m * hardSphereKappa ^ q

Canonical separated-block coordinates

def HsVirial.hardSphereBlockCoordinateEquiv (m q : ℕ) : (Fin (m * 2 + q) → HSPosition 3) ≃ᵐ (Fin m → HSPosition 3 × HSPosition 3) × (Fin q → HSPosition 3)

Split a position array into paired blocks and remaining single positions.

Equations

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

theorem HsVirial.measurePreserving_hardSphereBlockCoordinateEquiv (m q : ℕ) : MeasureTheory.MeasurePreserving (⇑(hardSphereBlockCoordinateEquiv m q)) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereBlockCoordinateEquiv_preimage_separatedBlockProductRegion_volume (m q : ℕ) : MeasureTheory.volume.real (⇑(hardSphereBlockCoordinateEquiv m q) ⁻¹' hardSphereSeparatedBlockProductRegion m q) = MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ m * hardSphereKappa ^ q

def HsVirial.hardSphereReindexedBlockCoordinateEquiv {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) : (Fin n → HSPosition 3) ≃ᵐ (Fin m → HSPosition 3 × HSPosition 3) × (Fin q → HSPosition 3)

Reindex a position array before separating paired and single blocks.

Equations

• HsVirial.hardSphereReindexedBlockCoordinateEquiv e = (MeasurableEquiv.piCongrLeft (fun (x : Fin n) => HsVirial.HSPosition 3) e).symm.trans (HsVirial.hardSphereBlockCoordinateEquiv m q)

theorem HsVirial.measurePreserving_hardSphereReindexedBlockCoordinateEquiv {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) : MeasureTheory.MeasurePreserving (⇑(hardSphereReindexedBlockCoordinateEquiv e)) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereReindexedBlockCoordinateEquiv_preimage_separatedBlockProductRegion_volume {n m q : ℕ} (e : Fin (m * 2 + q) ≃ Fin n) : MeasureTheory.volume.real (⇑(hardSphereReindexedBlockCoordinateEquiv e) ⁻¹' hardSphereSeparatedBlockProductRegion m q) = MeasureTheory.volume.real hardSphereSeparatedPairRegion ^ m * hardSphereKappa ^ q

The tree region in difference coordinates

theorem HsVirial.hardSphereCoordinateEquiv_apply {k : ℕ} (r : HardSphereConfiguration k 3) (i : Fin (k - 1)) (a : Fin 3) : (hardSphereCoordinateEquiv k) r (i, a) = (r i).ofLp a

theorem HsVirial.hardSphereTreeDifferenceFlatBlock_eq {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) (r : HardSphereConfiguration k 3) (i : Fin (k - 1)) : (fun (a : Fin 3) => (hardSphereTreeFlatDifferenceLinearMap hT) ((hardSphereCoordinateEquiv k) r) (i, a)) = fun (a : Fin 3) => (hardSphereTreeDifference hT r i).ofLp a

theorem HsVirial.hardSphereTreeRegion_subset_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)

noncomputable def HsVirial.hardSphereTreeFlatDifferenceMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : HardSphereConfiguration k 3 → Fin (k - 1) × Fin 3 → ℝ

Send an anchored configuration to its flattened tree-difference coordinates.

Equations

• HsVirial.hardSphereTreeFlatDifferenceMap hT r = (HsVirial.hardSphereTreeFlatDifferenceLinearMap hT) ((HsVirial.hardSphereCoordinateEquiv k) r)

theorem HsVirial.measurePreserving_hardSphereTreeFlatDifferenceMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.MeasurePreserving (hardSphereTreeFlatDifferenceMap hT) MeasureTheory.volume MeasureTheory.volume

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

Send an anchored configuration to the Euclidean differences along tree edges.

Equations

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

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

theorem HsVirial.measurePreserving_hardSphereTreeDifferencePositionMap {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.MeasurePreserving (hardSphereTreeDifferencePositionMap hT) MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.hardSphereTreeRegion_volume_le_flatProductBallRegion {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.volume (hardSphereTreeRegion T) ≤ MeasureTheory.volume (hardSphereFlatProductBallRegion (k - 1))

theorem HsVirial.hardSphereFlatProductBallRegion_subset_closedBall (n : ℕ) : hardSphereFlatProductBallRegion n ⊆ Metric.closedBall 0 1

theorem HsVirial.hardSphereFlatProductBallRegion_measure_ne_top (n : ℕ) : MeasureTheory.volume (hardSphereFlatProductBallRegion n) ≠ ⊤

theorem HsVirial.hardSphereTreeRegion_real_volume_le_kappa {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ treeUniverse) : MeasureTheory.volume.real (hardSphereTreeRegion T) ≤ hardSphereKappa ^ (k - 1)

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