The star anchor: stars satisfy the Sidorenko inequality (the Blakley-Roy case)
ProvedSDC.star_anchorThe Blakley-Roy anchor of the framework: stars satisfy Sidorenko inequality. For every finite nonempty host G and every number of leaves t, the homomorphism density of the star with t leaves in G is at least the t-th power of the edge density of G. This is the classical positive case of Sidorenko inequality (the star case, via the power mean inequality), and it validates the counting definitions of the framework before the search for a violating host begins.
import Mathlib import Definitions.Def_SDC_graphs import Definitions.Def_SDC_density
namespace SDC
/-! The Blakley-Roy anchor of the framework: stars satisfy Sidorenko
inequality. For every finite nonempty host G and every number of leaves
t, the homomorphism density of the star with t leaves in G is at least
the t-th power of the edge density of G. This is the classical positive
case of Sidorenko inequality (the star case, via the power mean
inequality), and it validates the counting definitions of the framework
before the search for a violating host begins. -/
theorem star_anchor (t : ℕ) {W : Type*} [Fintype W] [Nonempty W] (G : SimpleGraph W) :
(edgeDensity G) ^ t ≤ homDensity (starGraph t) G := by
sorry
end SDC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every number of leaves t, every finite nonempty vertex type W, and every simple graph G on W, the edge density of G raised to the t-th power is at most the homomorphism density of the star graph with t leaves in G.