The truncated distance kernel

Fix a finite graph G, a ratio q and a radius R. The kernel row of a vertex v (Cslib.Circuits.Frontier.Gaussian.kernelRow) is the vector z ↦ q ^ dist(v, z) of the Euclidean space over the vertices, cut off to 0 outside the closed ball of radius R around v. Distances are extended distances, so an unreachable vertex receives 0. The row of v has entry q ^ 0 = 1 at v, so its norm is at least one, and the unit kernel row (Cslib.Circuits.Frontier.Gaussian.unitKernelRow) divides it by its norm. These are the vectors of the Gaussian layouts of the frontier method: a vertex is scored by the inner product of its unit kernel row with a standard Gaussian vector.

Correlation of adjacent rows. For adjacent u and v the distances from u and from v to any vertex differ by at most one. Where both rows are nonzero their entries a, b are equal or differ by the factor q, and in either case a b ≥ κ (a ^ 2 + b ^ 2) / 2 with κ = 2 q / (1 + q ^ 2) ≤ 1. Where exactly one row is nonzero the vertex lies on a sphere of radius R around u or v; in maximum degree D ≥ 2 such a sphere has at most D (D - 1) ^ R vertices, so these vertices cost at most D ((D - 1) q ^ 2) ^ R in total (Cslib.Circuits.Frontier.Gaussian.le_inner_kernelRow). Dividing by the norms, for q ≥ 0 the unit rows of adjacent vertices have inner product at least κ - D ((D - 1) q ^ 2) ^ R (Cslib.Circuits.Frontier.Gaussian.le_inner_unitKernelRow). No girth assumption is needed. As R grows with (D - 1) q ^ 2 < 1 the error vanishes, and as q increases to 1 / √(D - 1) the correlation κ tends to 2 √(D - 1) / D.

Main definitions

• Cslib.Circuits.Frontier.Gaussian.kernelRow: the truncated distance kernel row of a vertex.
• Cslib.Circuits.Frontier.Gaussian.unitKernelRow: the kernel row divided by its norm.

Main results

• Cslib.Circuits.Frontier.Gaussian.norm_unitKernelRow: unit kernel rows are unit vectors.
• Cslib.Circuits.Frontier.Gaussian.unitKernelRow_eq_zero_of_lt: the unit kernel row of v vanishes outside the closed ball of radius R around v.
• Cslib.Circuits.Frontier.Gaussian.le_inner_kernelRow, Cslib.Circuits.Frontier.Gaussian.le_inner_unitKernelRow: the correlation of adjacent rows.

noncomputable def Cslib.Circuits.Frontier.Gaussian.kernelRow {V : Type u_1} (G : SimpleGraph V) (q : ℝ) (R : ℕ) (v : V) : EuclideanSpace ℝ V

The truncated distance kernel row of v: the vector z ↦ q ^ dist(v, z) of the Euclidean space over the vertices, cut off to 0 where the extended distance from v exceeds R.

noncomputable def Cslib.Circuits.Frontier.Gaussian.unitKernelRow {V : Type u_1} (G : SimpleGraph V) [Fintype V] (q : ℝ) (R : ℕ) (v : V) : EuclideanSpace ℝ V

The unit kernel row of v: its kernel row divided by its norm.

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_apply {V : Type u_1} {G : SimpleGraph V} (q : ℝ) (R : ℕ) (v z : V) : (kernelRow G q R v).ofLp z = if G.edist v z ≤ ↑R then q ^ G.dist v z else 0

@[simp]

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_self {V : Type u_1} {G : SimpleGraph V} (q : ℝ) (R : ℕ) (v : V) : (kernelRow G q R v).ofLp v = 1

The kernel row of v takes the value 1 at v.

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_nonneg {V : Type u_1} {G : SimpleGraph V} {q : ℝ} (hq : 0 ≤ q) (R : ℕ) (v z : V) : 0 ≤ (kernelRow G q R v).ofLp z

The kernel is nonnegative for a nonnegative ratio.

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_comm {V : Type u_1} {G : SimpleGraph V} (q : ℝ) (R : ℕ) (v z : V) : (kernelRow G q R v).ofLp z = (kernelRow G q R z).ofLp v

The kernel is symmetric.

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_eq_zero_of_lt {V : Type u_1} {G : SimpleGraph V} {q : ℝ} {R : ℕ} {v z : V} (h : ↑R < G.edist v z) : (kernelRow G q R v).ofLp z = 0

The kernel row of v vanishes outside the closed ball of radius R around v.

theorem Cslib.Circuits.Frontier.Gaussian.kernelRow_of_le {V : Type u_1} {G : SimpleGraph V} {q : ℝ} {R : ℕ} {v z : V} (h : G.edist v z ≤ ↑R) : (kernelRow G q R v).ofLp z = q ^ G.dist v z

Inside the closed ball of radius R around v, the kernel row of v is q ^ dist(v, z).

Correlation of adjacent rows

theorem Cslib.Circuits.Frontier.Gaussian.one_le_norm_kernelRow {V : Type u_1} {G : SimpleGraph V} [Fintype V] (q : ℝ) (R : ℕ) (v : V) : 1 ≤ ‖kernelRow G q R v‖

Every kernel row has norm at least one, from its entry 1 at its own vertex.

theorem Cslib.Circuits.Frontier.Gaussian.unitKernelRow_apply {V : Type u_1} {G : SimpleGraph V} [Fintype V] (q : ℝ) (R : ℕ) (v z : V) : (unitKernelRow G q R v).ofLp z = ‖kernelRow G q R v‖⁻¹ * (kernelRow G q R v).ofLp z

@[simp]

theorem Cslib.Circuits.Frontier.Gaussian.norm_unitKernelRow {V : Type u_1} {G : SimpleGraph V} [Fintype V] (q : ℝ) (R : ℕ) (v : V) : ‖unitKernelRow G q R v‖ = 1

Unit kernel rows are unit vectors.

theorem Cslib.Circuits.Frontier.Gaussian.unitKernelRow_eq_zero_of_lt {V : Type u_1} {G : SimpleGraph V} [Fintype V] {q : ℝ} {R : ℕ} {v z : V} (h : ↑R < G.edist v z) : (unitKernelRow G q R v).ofLp z = 0

The unit kernel row of v vanishes outside the closed ball of radius R around v.

theorem Cslib.Circuits.Frontier.Gaussian.unitKernelRow_nonneg {V : Type u_1} {G : SimpleGraph V} [Fintype V] {q : ℝ} (hq : 0 ≤ q) (R : ℕ) (v z : V) : 0 ≤ (unitKernelRow G q R v).ofLp z

The unit kernel is nonnegative for a nonnegative ratio.

theorem Cslib.Circuits.Frontier.Gaussian.le_inner_kernelRow {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {D : ℕ} (hD : 2 ≤ D) (hdeg : ∀ (v : V), G.degree v ≤ D) (q : ℝ) (R : ℕ) {u v : V} (huv : G.Adj u v) : 2 * q / (1 + q ^ 2) * (‖kernelRow G q R u‖ ^ 2 + ‖kernelRow G q R v‖ ^ 2) / 2 - ↑D * ((↑D - 1) * q ^ 2) ^ R ≤ inner ℝ (kernelRow G q R u) (kernelRow G q R v)

Correlation of adjacent kernel rows. In a graph of maximum degree D ≥ 2, the kernel rows of adjacent vertices have inner product at least κ = 2 q / (1 + q ^ 2) times the mean of their squared norms, up to the error D ((D - 1) q ^ 2) ^ R of the truncation spheres.

theorem Cslib.Circuits.Frontier.Gaussian.le_inner_unitKernelRow {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {D : ℕ} (hD : 2 ≤ D) (hdeg : ∀ (v : V), G.degree v ≤ D) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) {u v : V} (huv : G.Adj u v) : 2 * q / (1 + q ^ 2) - ↑D * ((↑D - 1) * q ^ 2) ^ R ≤ inner ℝ (unitKernelRow G q R u) (unitKernelRow G q R v)

Correlation of adjacent unit kernel rows. In a graph of maximum degree D ≥ 2 and for a nonnegative ratio q, the unit kernel rows of adjacent vertices have inner product at least 2 q / (1 + q ^ 2) - D ((D - 1) q ^ 2) ^ R.