Extremal inequalities for graphons

This file records the first analytic extremal consequences of the graphon API. The main results are Goodman's inequality

t(K₃, W) ≥ 2 * t(K₂, W)^2 - t(K₂, W),

and Sidorenko's inequality for the four-cycle. Goodman's proof writes the nonnegative integral ∫ W(x,y) (1 - W(x,z)) (1 - W(y,z)) in two ways and uses Cauchy--Schwarz for the degree function, followed by Mantel's triangle-free corollary. The four-cycle proof identifies its density with the integral of the square of a two-step kernel and applies two second-moment inequalities. All statements are for arbitrary probability carriers; no atomlessness or standard Borel assumption is involved.

They use only the strict graphon carrier and its edge, triangle, and product-integral APIs.

Main results

• goodman_triangle_density — Goodman's lower bound for triangle density;
• mantel_triangle_free — a triangle-free graphon has edge density at most 1 / 2.
• sidorenko_cycleGraph_four — the 4-cycle density is at least the fourth power of edge density.

References

• A. Goodman, "On sets of acquaintances and strangers at a party", American Mathematical Monthly 66 (1959), 778--783; see also L. Lovász, Large Networks and Graph Limits, §7.2.
• Y. Zhao, Graph Theory and Additive Combinatorics, Cambridge University Press (2023), Theorem 5.2.1, online notes.

The public extremal inequalities.

theorem TauCeti.DenseGraphLimits.goodman_triangle_density {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : 2 * homDensity ⊤ W ^ 2 - homDensity ⊤ W ≤ homDensity ⊤ W

Goodman's inequality. For every graphon, triangle density is at least 2 * t(K₂, W)^2 - t(K₂, W).

theorem TauCeti.DenseGraphLimits.mantel_triangle_free {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (htriangle : homDensity ⊤ W = 0) : homDensity ⊤ W ≤ 1 / 2

Mantel's inequality for graphons. A graphon with zero triangle density has edge density at most 1 / 2.

The four-cycle inequality

theorem TauCeti.DenseGraphLimits.sidorenko_cycleGraph_four {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity (SimpleGraph.cycleGraph 4) W ≥ homDensity ⊤ W ^ 4

Sidorenko's inequality for the 4-cycle. The 4-cycle homomorphism density is at least the fourth power of the edge density, on every probability carrier. This is the graphon form of the K_{2,2} case in Y. Zhao, Graph Theory and Additive Combinatorics, Theorem 5.2.1.