Bipartite multigraphs with expander-like properties

This note considers the following combinatorial question: “For which integers dd and functions fdfd does there exist, for every large enough vv, a bipartite dd-regular multigraph on 2v2v nodes with node sets VV and WW having the following property: For every UU that is a subset of either VV or WW, the cardinality of the set of neighbours of UU is at least fd(|U|)fd(|U|)?” Graphs with the above property seem to behave well also with respect to other, more complicated, expander-like properties. We provide results for dd in {5,6,7,8} and give a description of a fairly general methodology for devising computer-assisted proofs for a wide class of mathematical claims using interval arithmetic.