Documentation

TauCeti.Combinatorics.Regularity.Graphon.Energy

Finite partition energy as graphon partition energy #

For a graph G on Fin m with 0 < m, the graphon finiteGraphGraphon G takes the adjacency value of G on the products of the m equal cells of the unit interval. A partition P of the vertices lifts to the partition P.cellPartition of the unit interval whose parts are the unions of the cells over each part of P. Over the cells of two vertex sets A and B, the graphon averages to the edge density d_G(A, B), so the block-average step graphon of G over P.cellPartition takes the value d_G(P.part i, P.part j) on the cells of i and j. Its L² norm squared is therefore the size-weighted finite energy, diagonal blocks included.

This module depends on both the finite regularity energy and the graphon energy; neither theory imports the other.

The lifted partition Finpartition.cellPartition is defined with the other unit-interval cell infrastructure, in TauCeti.MeasureTheory.Constructions.UnitInterval.CellPartition.

Main results #

source
theorem SimpleGraph.setAverage_finiteGraphGraphon_preimage {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) [DecidableRel G.Adj] (A B : Finset (Fin m)) :
⨍ (z : ↑unitInterval × ↑unitInterval) in (TauCeti.unitInterval.cellFin m ⁻¹' ↑A) ×ˢ (TauCeti.unitInterval.cellFin m ⁻¹' ↑B), (TauCeti.DenseGraphLimits.finiteGraphGraphon G) z.1 z.2 ∂MeasureTheory.volume.prod MeasureTheory.volume = ↑(G.edgeDensity A B)

Block averages of the graphon of a finite graph. Over the cells of two vertex sets A and B, the graphon of G averages to the edge density d_G(A, B). When either set is empty, both sides are 0.

source
theorem SimpleGraph.stepGraphonAvg_finiteGraphGraphon_cellPartition_apply {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (x y : ↑unitInterval) :
(TauCeti.DenseGraphLimits.stepGraphonAvg P.cellPartition ⋯ (TauCeti.DenseGraphLimits.finiteGraphGraphon G)) x y = ↑(G.edgeDensity (P.part (TauCeti.unitInterval.cellFin m x)) (P.part (TauCeti.unitInterval.cellFin m y)))

The block averages of the graphon of a finite graph. Over the lifted partition P.cellPartition, the block-average step graphon of G takes at (x, y) the edge density between the parts of P containing the cells of x and y.

source
theorem SimpleGraph.graphonPartitionEnergy_finiteGraphGraphon {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) [DecidableRel G.Adj] (P : Finpartition Finset.univ) :
TauCeti.DenseGraphLimits.graphonPartitionEnergy MeasureTheory.volume P.cellPartition ⋯ (TauCeti.DenseGraphLimits.finiteGraphGraphon G) = G.weightedEnergy P

Finite partition energy is graphon partition energy. For a graph G on Fin m with 0 < m and a partition P of its vertices, the size-weighted energy of P is the partition energy of the graphon of G over the partition of the unit interval grouping the vertex cells by the parts of P.

source
theorem SimpleGraph.graphonPartitionEnergy_finiteGraphGraphon_comap_symm {m : ℕ} [NeZero m] {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : V ≃ Fin m) (P : Finpartition Finset.univ) :
TauCeti.DenseGraphLimits.graphonPartitionEnergy MeasureTheory.volume (Finpartition.comap (⇑e.symm) (P.copy ⋯)).cellPartition ⋯ (TauCeti.DenseGraphLimits.finiteGraphGraphon (SimpleGraph.comap (⇑e.symm) G)) = G.weightedEnergy P

Finite partition energy as graphon partition energy, on any finite vertex type. Relabel the vertices of G along an equivalence e : V ≃ Fin m with 0 < m. The size-weighted energy of P is then the graphon partition energy of the relabelled graph over the cell partition of the relabelled P. For a nonempty finite V, take e := Fintype.equivFin V.