Sidorenko's conjecture holds for a blow-up of every bipartite graph (Corollary 1.3)
ProvedSidB.blowup_sidorenkoCorollary 1.3 of the paper, the title result: for every bipartite graph H with bipartition A union B there is a positive integer p such that the blow-up H_A^p satisfies Sidorenko's conjecture; in the paper, p = |A|! always suffices. The blown-up right vertices have degrees p times the original degrees, and since C(|A|, r) C(r, k) divides |A|! r! for each k - equivalently, since C(|A|, k) C(|A|-k, r-k) divides the blown-up degree counts - the divisibility criterion of Theorem 1.1 applies to the blow-up. The L^p reading of the introduction: the statement says that for every bipartite graph the expectation of the rho-density functional to the power p bounds the edge density to the power p times the edge count, for the p furnished by the corollary; that is exactly the homomorphism Sidorenko inequality for the blow-up.
Formalization Note The goal is stated existentially over p; the paper's proof of Corollary 1.3 through the factorial blow-up is the proposed work of the goal, consuming the divisibility conjunct of the preceding milestone.
import Mathlib import Definitions.Def_SidB_graph import Definitions.Def_SidB_hyper
namespace SidB
/-! The goal (Corollary 1.3): Sidorenko's conjecture holds for a blow-up
of every bipartite graph. For every bipartite graph H there is a positive
integer p such that the blow-up of H relative to its left part satisfies
Sidorenko. In the paper p = |A|! always suffices: the degrees of the
blown-up right vertices are multiplied by p, so the divisibility conditions
of Theorem 1.1 hold for the blow-up with p = |A|!, and the L^p reading of
Corollary 1.3 - the expected rho-density to the power p against the edge
density to the power p times the edge count - is exactly the homomorphism
density of the blow-up. -/
theorem blowup_sidorenko {A B : Type} [Fintype A] [Fintype B] (H : Bigraph A B) :
∃ p : ℕ, SatisfiesSidorenko (H.blowUp p) := by sorry
end SidB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every bipartite graph H with finite parts, there exists a natural number p such that the blow-up of H - the bigraph on the same left part whose right part is the original right part times Fin p, a left vertex adjacent to a pair exactly when it is adjacent to the first component - satisfies Sidorenko: for every graphon, the homomorphism density of the blow-up is at least the edge density of the graphon raised to the power of the number of edges of the blow-up. No hypotheses appear.
The statement is ∃ p : ℕ, SatisfiesSidorenko (H.blowUp p) with no hypothesis 0 < p. With p = 0 the right part B × Fin 0 is empty, g.dens (H.blowUp 0) = 1 by exp_one, (H.blowUp 0).edgeCount = 0 and g.edgeDens ^ 0 = 1, so the statement holds for every H trivially; this is the accepted proof on the platform. Corollary 1.3 requires a positive integer p (the paper gives p = |A|!). The intended statement is ∃ p : ℕ, 0 < p ∧ SatisfiesSidorenko (H.blowUp p).