HardSphereMeasure

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

def HsVirial.hardSphereIndexEquiv (k d : ℕ) : Fin (k - 1) × Fin d ≃ Fin ((k - 1) * d)

The standard finite-index coordinate equivalence used to flatten a hard-sphere configuration.

Equations

• HsVirial.hardSphereIndexEquiv k d = finProdFinEquiv

theorem HsVirial.measurePreserving_curry_pi {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Fintype ι] [Fintype κ] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.curry ι κ α).symm) (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.Measure.pi fun (x : κ) => μ) (MeasureTheory.Measure.pi fun (x : ι × κ) => μ)

A finite product of finite product measures is unchanged by currying.

def HsVirial.hardSphereFlattenEquiv (k d : ℕ) : HardSphereConfiguration k d ≃ᵐ EuclideanSpace ℝ (Fin ((k - 1) * d))

The measurable equivalence from the anchored product of Euclidean spaces to the usual flat Euclidean coordinate space. The map only reindexes coordinates: first each Euclidean block is represented by its real coordinates, then the two finite indices are flattened.

Equations

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

theorem HsVirial.measurePreserving_hardSphereFlattenEquiv (k d : ℕ) : MeasureTheory.MeasurePreserving (⇑(hardSphereFlattenEquiv k d)) MeasureTheory.volume MeasureTheory.volume

The coordinate flattening preserves the canonical product Lebesgue measure on the anchored configuration space.

theorem HsVirial.measure_image_eq_of_measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) (h : MeasureTheory.MeasurePreserving (⇑e) μ ν) {s : Set α} (hs : MeasurableSet s) : ν (⇑e '' s) = μ s

A measure-preserving measurable equivalence preserves the volume of every measurable subset.

theorem HsVirial.hardSphereNBCRegion_flatten_volume {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : MeasureTheory.volume (⇑(hardSphereFlattenEquiv k d) '' nbcRegion hardSphereActiveExact T) = MeasureTheory.volume (nbcRegion hardSphereActiveExact T)

In particular, every measurable NBC region has the same volume after the coordinate flattening.

noncomputable def HsVirial.hardSphereNBCVolumeFlat {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : ℝ

The same NBC-region volume computed in the flat Euclidean model.

Equations

• HsVirial.hardSphereNBCVolumeFlat T = MeasureTheory.volume.real (⇑(HsVirial.hardSphereFlattenEquiv k d) '' HsVirial.nbcRegion HsVirial.hardSphereActiveExact T)

theorem HsVirial.hardSphereNBCVolumeFlat_eq {k d : ℕ} [NeZero k] (T : Finset (Sym2 (Fin k))) : hardSphereNBCVolumeFlat T = hardSphereNBCVolume T

theorem HsVirial.hardSphere_nbc_volume_identity_flat {k d : ℕ} (hk : 2 ≤ k) : have x := ⋯; ↑k.factorial * |hardSphereBk| = ∑ T ∈ treeUniverse, hardSphereNBCVolumeFlat T

The NBC identity is unchanged when the configuration measure is written on the flat Euclidean coordinate space.