Asymmetric Sidorenko, graphs and graphons (Proposition 22)
ProvedDirS.asym_sid_graphonProposition 22 of the paper: the bipartite counterpart of Proposition 21. The bipartite graph A has the asymmetric Sidorenko property if and only if for every graphon W, t_bip(A,W) >= |E W|^{e(A)}. The proof is the same approximation argument run on bipartite graphs: the bipartite graphon of a finite bipartite graph witnesses the backward direction, and the approximation scheme of Theorem 13 with the counting Lemma 18 carries the forward direction. In the mission the statement runs through the bipartite side of the graph world interface, consuming the bipartite approximation axioms.
Formalization Note The asymmetric Sidorenko property quantifies only over bipartite graphs H with their two parts; the graphon inequality quantifies over all kernels, symmetric or not.
import Mathlib import Definitions.Def_DirS_gr import Definitions.Def_DirS_gw
namespace DirS
/-! Milestone 3 (Proposition 22): asymmetric Sidorenko, graphs and
graphons. The bipartite graph A has the asymmetric Sidorenko property if
and only if for every directed graphon the bipartite A-density is at
least the absolute mean of the kernel to the power e(A). The proof is the
bipartite counterpart of Proposition 21, running through the bipartite
graphon of a finite bipartite graph and the bipartite approximation
scheme of the world. -/
theorem asym_sid_graphon {mA nA : ℕ} (A : BipGraph mA nA) (_w : GraphWorld) :
AsymSidorenko A ↔ AsymSidW A := by sorry
end DirS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every bipartite graph A with two finite parts, and every graph world, A has the asymmetric Sidorenko property - for every bipartite graph H, the part-respecting homomorphism density of A in H is at least the bipartite edge density of H to the power e(A) - if and only if for every directed graphon, the bipartite A-density is at least the absolute mean of the kernel to the power e(A). No other hypotheses appear.
The hypothesis (_w : GraphWorld) has an empty type (see DirS_gw), so the statement is vacuous and carries none of the content of Proposition 22.