This file is the finite Mayer/NBC bridge. The graph part is completely discrete. The measure part is stated for an arbitrary configuration space; its only analytic input is measurability of the finitely many regions that occur in the finite tree sum.

The finite graph ledger

noncomputable def HsVirial.connectedEdgeSubsets {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : Finset (Finset (Sym2 V))

The finite collection of edge subsets inducing a connected graph.

Equations

• HsVirial.connectedEdgeSubsets G = {A ∈ (HsVirial.graphEdgeFinset G).powerset | (SimpleGraph.fromEdgeSet ↑A).Connected}

noncomputable def HsVirial.m {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : ℤ

The alternating sum of connected spanning edge subsets.

Equations

• HsVirial.m G = ∑ A ∈ HsVirial.connectedEdgeSubsets G, HsVirial.matroidParitySign A.card

def HsVirial.activeEdge {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) (e : Sym2 V) : Prop

An edge of the complete graph marked active by the overlap data.

Equations

• HsVirial.activeEdge x e = (e ∈ HsVirial.graphEdgeFinset (SimpleGraph.completeGraph V) ∧ x e = true)

noncomputable def HsVirial.activeEdgeFinset {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) : Finset (Sym2 V)

The finite set of active edges.

Equations

• HsVirial.activeEdgeFinset x = Finset.filter (HsVirial.activeEdge x) Finset.univ

def HsVirial.overlapGraph {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) : SimpleGraph V

The graph whose edges are precisely the active overlaps.

Equations

• HsVirial.overlapGraph x = SimpleGraph.fromEdgeSet ↑(HsVirial.activeEdgeFinset x)

theorem HsVirial.activeEdgeFinset_subset_complete {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) : activeEdgeFinset x ⊆ graphEdgeFinset (SimpleGraph.completeGraph V)

theorem HsVirial.graphEdgeFinset_overlapGraph {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) : graphEdgeFinset (overlapGraph x) = activeEdgeFinset x

theorem HsVirial.edgeSet_overlapGraph {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) : (overlapGraph x).edgeSet = ↑(activeEdgeFinset x)

theorem HsVirial.matroidParitySign_eq_neg_one_pow (n : ℕ) : matroidParitySign n = (-1) ^ n

noncomputable def HsVirial.bond {V : Type u_1} [Fintype V] (x : Sym2 V → Bool) (e : Sym2 V) : ℤ

The Mayer bond: minus one for an active edge and zero otherwise.

Equations

• HsVirial.bond x e = if HsVirial.activeEdge x e then -1 else 0

noncomputable def HsVirial.completeConnectedEdgeSubsets {V : Type u_1} [Fintype V] [DecidableEq V] : Finset (Finset (Sym2 V))

The connected spanning edge subsets of the complete graph.

Equations

• HsVirial.completeConnectedEdgeSubsets = HsVirial.connectedEdgeSubsets (SimpleGraph.completeGraph V)

noncomputable def HsVirial.mayerKernel {V : Type u_1} [Fintype V] [DecidableEq V] (x : Sym2 V → Bool) : ℤ

Sum the products of Mayer bonds over connected spanning edge sets.

Equations

• HsVirial.mayerKernel x = ∑ A ∈ HsVirial.completeConnectedEdgeSubsets, ∏ e ∈ A, HsVirial.bond x e

theorem HsVirial.bond_prod_of_subset_active {V : Type u_1} [Fintype V] {x : Sym2 V → Bool} {A : Finset (Sym2 V)} (hA : A ⊆ activeEdgeFinset x) : ∏ e ∈ A, bond x e = matroidParitySign A.card

theorem HsVirial.bond_prod_eq_zero_of_not_subset_active {V : Type u_1} [Fintype V] {x : Sym2 V → Bool} {A : Finset (Sym2 V)} (hA : ¬A ⊆ activeEdgeFinset x) : ∏ e ∈ A, bond x e = 0

theorem HsVirial.bond_eq_zero_of_not_active {V : Type u_1} [Fintype V] {x : Sym2 V → Bool} {e : Sym2 V} (he : ¬activeEdge x e) : bond x e = 0

theorem HsVirial.connectedEdgeSubsets_overlap {V : Type u_1} [Fintype V] [DecidableEq V] (x : Sym2 V → Bool) : connectedEdgeSubsets (overlapGraph x) = {A ∈ completeConnectedEdgeSubsets | A ⊆ activeEdgeFinset x}

theorem HsVirial.mayerKernel_eq_m {V : Type u_1} [Fintype V] [DecidableEq V] (x : Sym2 V → Bool) : mayerKernel x = m (overlapGraph x)

Concrete NBC bases of the graphic matroid

def HsVirial.IsGraphCircuitNBCandidate {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) (e : Sym2 V) : Prop

An edge completing a broken circuit already contained in the specified edge set.

Equations

• HsVirial.IsGraphCircuitNBCandidate G A e = ∃ (C : Finset (Sym2 V)), HsVirial.IsGraphCircuit G C ∧ e ∈ C ∧ (∀ f ∈ C, HsVirial.graphEdgeLE f e) ∧ ↑(C.erase e) ⊆ ↑A

def HsVirial.IsGraphCircuitNBCBad {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

The edge set contains a broken circuit in the circuit-based formulation.

Equations

• HsVirial.IsGraphCircuitNBCBad G A = ∃ (e : Sym2 V), HsVirial.IsGraphCircuitNBCandidate G A e

def HsVirial.IsExplicitNBCBase {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

A spanning forest containing no broken circuit.

Equations

• HsVirial.IsExplicitNBCBase G A = (HsVirial.IsGraphForest G A ∧ HsVirial.IsGraphSpanning G A ∧ ¬HsVirial.IsGraphCircuitNBCBad G A)

def HsVirial.IsExplicitNBCTree {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

A connected spanning forest containing no broken circuit.

Equations

• HsVirial.IsExplicitNBCTree G A = (HsVirial.IsGraphForest G A ∧ (SimpleGraph.fromEdgeSet ↑A).Connected ∧ ¬HsVirial.IsGraphCircuitNBCBad G A)

noncomputable def HsVirial.graphNBCBaseSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) : Finset (Finset (Sym2 V))

Enumerate the no-broken-circuit bases of the graph.

Equations

• HsVirial.graphNBCBaseSubsets G = Finset.filter (HsVirial.IsExplicitNBCBase G) (HsVirial.graphEdgeFinset G).powerset

noncomputable def HsVirial.graphNBCTreeSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) : Finset (Finset (Sym2 V))

Enumerate the no-broken-circuit spanning trees of the graph.

Equations

• HsVirial.graphNBCTreeSubsets G = Finset.filter (HsVirial.IsExplicitNBCTree G) (HsVirial.graphEdgeFinset G).powerset

noncomputable def HsVirial.NBC {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) : ℕ

The number of no-broken-circuit spanning trees.

Equations

• HsVirial.NBC G = (HsVirial.graphNBCTreeSubsets G).card

theorem HsVirial.graphicMatroid_spanning_iff_graphSpanning {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : A ⊆ graphEdgeFinset G) : (graphicMatroid G).Spanning ↑A ↔ IsGraphSpanning G A

theorem HsVirial.graphSpanning_iff_connected_of_connected {V : Type u_1} [Fintype V] {G : SimpleGraph V} (hG : G.Connected) {A : Finset (Sym2 V)} (_hA : A ⊆ graphEdgeFinset G) : IsGraphSpanning G A ↔ (SimpleGraph.fromEdgeSet ↑A).Connected

theorem HsVirial.graphNBCTreeSubsets_eq_graphNBCBaseSubsets_of_connected {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} (hG : G.Connected) : graphNBCTreeSubsets G = graphNBCBaseSubsets G

theorem HsVirial.nbcBaseSubsets_graphic_eq_graphNBCBaseSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) : nbcBaseSubsets (graphicMatroid G) = graphNBCBaseSubsets G

noncomputable def HsVirial.treeUniverse {V : Type u_1} [Fintype V] : Finset (Finset (Sym2 V))

The finite collection of spanning trees on the ambient vertex set.

Equations

• HsVirial.treeUniverse = {T ∈ (HsVirial.graphEdgeFinset (SimpleGraph.completeGraph V)).powerset | (SimpleGraph.fromEdgeSet ↑T).IsTree}

theorem HsVirial.graphNBCTreeSubsets_subset_treeUniverse {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : A ∈ graphNBCTreeSubsets G) : A ∈ treeUniverse

The signed matroid theorem is now applied to the concrete graphic construction. The good sets on the right are a finite, explicit filter; NBC is its natural cardinality.

theorem HsVirial.graphNBCBaseSubsets_card_eq_NBC_of_connected {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} (hG : G.Connected) : (graphNBCBaseSubsets G).card = NBC G

theorem HsVirial.m_eq_signed_NBC_of_connected {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} (hG : G.Connected) : m G = (-1) ^ (Fintype.card V - 1) * ↑(NBC G)

Pointwise finite tree decomposition

def HsVirial.nbcRegion {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} (active : X → Sym2 V → Bool) (T : Finset (Sym2 V)) : Set X

Configurations whose overlap graph has the specified no-broken-circuit spanning tree.

Equations

• HsVirial.nbcRegion active T = {x : X | HsVirial.IsExplicitNBCTree (HsVirial.overlapGraph (active x)) T}

theorem HsVirial.mem_treeUniverse_of_mem_graphNBCTreeSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {x : Sym2 V → Bool} {T : Finset (Sym2 V)} (hT : T ∈ graphNBCTreeSubsets (overlapGraph x)) : T ∈ treeUniverse

theorem HsVirial.mem_graphNBCTreeSubsets_iff_mem_treeUniverse_and_region {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} (active : X → Sym2 V → Bool) (x : X) {T : Finset (Sym2 V)} (_hT : T ∈ treeUniverse) : T ∈ graphNBCTreeSubsets (overlapGraph (active x)) ↔ x ∈ nbcRegion active T

theorem HsVirial.nbc_tree_decomposition' {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (x : Sym2 V → Bool) : (if (overlapGraph x).Connected then NBC (overlapGraph x) else 0) = ∑ T ∈ treeUniverse, if T ∈ graphNBCTreeSubsets (overlapGraph x) then 1 else 0

The Boolean region form of the same decomposition.

theorem HsVirial.nbc_tree_decomposition_region {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} (active : X → Sym2 V → Bool) (x : X) : (if (overlapGraph (active x)).Connected then NBC (overlapGraph (active x)) else 0) = ∑ T ∈ treeUniverse, if x ∈ nbcRegion active T then 1 else 0

For disconnected overlap graphs both sides vanish. This is the finite form needed to turn the signed identity into a nonnegative integrand.

theorem HsVirial.graphNBC_zero_of_not_connected {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} (hG : ¬G.Connected) : NBC G = 0

def HsVirial.intMagnitude (z : ℤ) : ENNReal

The absolute value of an integer as an extended nonnegative real.

Equations

• HsVirial.intMagnitude z = ↑z.natAbs

theorem HsVirial.intMagnitude_signed_nat (n q : ℕ) : intMagnitude ((-1) ^ n * ↑q) = ↑q

theorem HsVirial.abs_mayerKernel_eq_nbc {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (x : Sym2 V → Bool) : intMagnitude (mayerKernel x) = if (overlapGraph x).Connected then ↑(NBC (overlapGraph x)) else 0

Arbitrary measure spaces

noncomputable def HsVirial.absMayerIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] {X : Type u_2} (active : X → Sym2 V → Bool) (x : X) : ENNReal

The absolute value of the configuration's Mayer kernel.

Equations

• HsVirial.absMayerIntegrand active x = HsVirial.intMagnitude (HsVirial.mayerKernel (active x))

noncomputable def HsVirial.absClusterCoefficient {V : Type u_1} [Fintype V] [DecidableEq V] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) : ENNReal

The integral of the absolute Mayer kernel, normalized by the vertex factorial.

Equations

• HsVirial.absClusterCoefficient μ active = (↑(Fintype.card V).factorial)⁻¹ * ∫⁻ (x : X), HsVirial.absMayerIntegrand active x ∂μ

theorem HsVirial.measurable_nbcRegion_indicator {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} [MeasurableSpace X] (active : X → Sym2 V → Bool) {T : Finset (Sym2 V)} (_hT : T ∈ treeUniverse) (hmeas : MeasurableSet (nbcRegion active T)) : Measurable ((nbcRegion active T).indicator fun (x : X) => 1)

theorem HsVirial.lintegral_abs_mayerKernel_eq_sum_NBC_region_measure {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) (hmeas : ∀ T ∈ treeUniverse, MeasurableSet (nbcRegion active T)) : ∫⁻ (x : X), absMayerIntegrand active x ∂μ = ∑ T ∈ treeUniverse, μ (nbcRegion active T)

theorem HsVirial.factorial_mul_absClusterCoefficient {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) (hmeas : ∀ T ∈ treeUniverse, MeasurableSet (nbcRegion active T)) : ↑(Fintype.card V).factorial * absClusterCoefficient μ active = ∑ T ∈ treeUniverse, μ (nbcRegion active T)

@[reducible, inline]

noncomputable abbrev HsVirial.absBk {V : Type u_1} [Fintype V] [DecidableEq V] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) : ENNReal

The absolute cluster coefficient in the notation of the volume identity.

Equations

• HsVirial.absBk μ active = HsVirial.absClusterCoefficient μ active

@[reducible, inline]

abbrev HsVirial.nbcRegionVolume {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) (T : Finset (Sym2 V)) : ENNReal

The measure of a no-broken-circuit tree region.

Equations

• HsVirial.nbcRegionVolume μ active T = μ (HsVirial.nbcRegion active T)

theorem HsVirial.factorial_mul_absBk_eq_nbcVolumeSum {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (active : X → Sym2 V → Bool) (hmeas : ∀ T ∈ treeUniverse, MeasurableSet (nbcRegion active T)) : ↑(Fintype.card V).factorial * absBk μ active = ∑ T ∈ treeUniverse, nbcRegionVolume μ active T

Hard-sphere activity, with no geometric factorization claim

@[reducible, inline]

abbrev HsVirial.HSPosition (d : ℕ) : Type

Euclidean position space in the specified dimension.

Equations

• HsVirial.HSPosition d = EuclideanSpace ℝ (Fin d)

def HsVirial.AnchoredHSConfiguration (k d : ℕ) : Type

Particle configurations whose distinguished particle is fixed at zero.

Equations

• HsVirial.AnchoredHSConfiguration k d = { r : Fin (k + 1) → HsVirial.HSPosition d // r 0 = 0 }

noncomputable def HsVirial.hardSphereActive {k d : ℕ} (r : AnchoredHSConfiguration k d) : Sym2 (Fin (k + 1)) → Bool

The overlap indicators of an explicitly anchored configuration.

Equations

• HsVirial.hardSphereActive r = Sym2.lift ⟨fun (i j : Fin (k + 1)) => decide (‖↑r i - ↑r j‖ < 1), ⋯⟩

@[simp]

theorem HsVirial.hardSphereActive_mk {k d : ℕ} (r : AnchoredHSConfiguration k d) (i j : Fin (k + 1)) : hardSphereActive r s(i, j) = decide (‖↑r i - ↑r j‖ < 1)

theorem HsVirial.hardSphere_mayerKernel_bridge {k d : ℕ} (r : AnchoredHSConfiguration k d) : mayerKernel (hardSphereActive r) = m (overlapGraph (hardSphereActive r))

theorem HsVirial.hardSphere_factorial_measure_bridge {k d : ℕ} [LinearOrder (Sym2 (Fin (k + 1)))] [MeasurableSpace (AnchoredHSConfiguration k d)] (μ : MeasureTheory.Measure (AnchoredHSConfiguration k d)) (hmeas : ∀ T ∈ treeUniverse, MeasurableSet (nbcRegion hardSphereActive T)) : ↑(Fintype.card (Fin (k + 1))).factorial * absClusterCoefficient μ hardSphereActive = ∑ T ∈ treeUniverse, μ (nbcRegion hardSphereActive T)