The truncated distance kernel

Fix a graph H, a ratio q and a radius R. The kernel row of a vertex v is the vector z ↦ q ^ dist(v, z), cut off to 0 outside the ball of radius R around v. The unit kernel row divides it by its Euclidean norm. Distances are extended distances, so an unreachable vertex lies in no sphere or ball and receives 0. The row of v has entry q ^ 0 = 1 at v, so its norm is at least one.

In a graph of maximum degree three:

• Growth (card_sphere_le, card_ball_le). The sphere of radius d has at most 3 * 2 ^ d vertices. A vertex at distance d + 1 has a neighbour at distance d, the penultimate vertex of a shortest walk; so a vertex at positive distance d has at most two neighbours at distance d + 1.
• Correlation (sum_kernel_mul_ge, sum_unitKernel_mul_ge). 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 κ = 2q / (1 + q ^ 2) ≤ 1. Where exactly one row is nonzero the vertex lies on a truncation sphere of radius R, and the growth bound charges these vertices at most 3 (2 q ^ 2) ^ R in total. Dividing by the norms, for q ≥ 0 the unit rows of adjacent vertices have inner product at least κ - 3 (2 q ^ 2) ^ R. No girth assumption is needed.

The ball lemmas ball_subset_ball_of_adj and mem_ball_of_not_disjoint bound the vertices on which a row, or a pair of rows, depends.

The _degree variants prove the same statements in maximum degree D ≥ 2, replacing the sphere bound by D * (D - 1) ^ d and the correlation error by D * ((D - 1) * q ^ 2) ^ R.

noncomputable def Complexity.Frontier.Gaussian.kernel {W : Type} (H : SimpleGraph W) (q : ℝ) (R : ℕ) (v z : W) : ℝ

The truncated distance kernel: q ^ dist(v, z) when the extended distance from v to z is at most R, and 0 otherwise.

Equations

• Complexity.Frontier.Gaussian.kernel H q R v z = if H.edist v z ≤ ↑R then q ^ H.dist v z else 0

theorem Complexity.Frontier.Gaussian.kernel_self {W : Type} (H : SimpleGraph W) (q : ℝ) (R : ℕ) (v : W) : kernel H q R v v = 1

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

theorem Complexity.Frontier.Gaussian.kernel_nonneg {W : Type} (H : SimpleGraph W) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) (v z : W) : 0 ≤ kernel H q R v z

The kernel is nonnegative for a nonnegative ratio.

theorem Complexity.Frontier.Gaussian.kernel_comm {W : Type} (H : SimpleGraph W) (q : ℝ) (R : ℕ) (v z : W) : kernel H q R v z = kernel H q R z v

The kernel is symmetric.

noncomputable def Complexity.Frontier.Gaussian.sphere {W : Type} (H : SimpleGraph W) [Fintype W] (v : W) (d : ℕ) : Finset W

The vertices at extended distance exactly d from v.

Equations

• Complexity.Frontier.Gaussian.sphere H v d = {z : W | H.edist v z = ↑d}

noncomputable def Complexity.Frontier.Gaussian.ball {W : Type} (H : SimpleGraph W) [Fintype W] (v : W) (r : ℕ) : Finset W

The vertices at extended distance at most r from v.

Equations

• Complexity.Frontier.Gaussian.ball H v r = {z : W | H.edist v z ≤ ↑r}

noncomputable def Complexity.Frontier.Gaussian.unitKernel {W : Type} (H : SimpleGraph W) [Fintype W] (q : ℝ) (R : ℕ) (v z : W) : ℝ

The kernel row of v divided by its Euclidean norm.

Equations

• Complexity.Frontier.Gaussian.unitKernel H q R v z = Complexity.Frontier.Gaussian.kernel H q R v z / √(∑ y : W, Complexity.Frontier.Gaussian.kernel H q R v y ^ 2)

@[simp]

theorem Complexity.Frontier.Gaussian.mem_sphere {W : Type} [Fintype W] (H : SimpleGraph W) {v z : W} {d : ℕ} : z ∈ sphere H v d ↔ H.edist v z = ↑d

@[simp]

theorem Complexity.Frontier.Gaussian.mem_ball {W : Type} [Fintype W] (H : SimpleGraph W) {v z : W} {r : ℕ} : z ∈ ball H v r ↔ H.edist v z ≤ ↑r

theorem Complexity.Frontier.Gaussian.mem_ball_self {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) (r : ℕ) : v ∈ ball H v r

theorem Complexity.Frontier.Gaussian.mem_ball_comm {W : Type} [Fintype W] (H : SimpleGraph W) {v z : W} {r : ℕ} : z ∈ ball H v r ↔ v ∈ ball H z r

theorem Complexity.Frontier.Gaussian.ball_mono {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) {r r' : ℕ} (h : r ≤ r') : ball H v r ⊆ ball H v r'

theorem Complexity.Frontier.Gaussian.sphere_subset_ball {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) (r : ℕ) : sphere H v r ⊆ ball H v r

theorem Complexity.Frontier.Gaussian.sphere_zero {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) : sphere H v 0 = {v}

theorem Complexity.Frontier.Gaussian.ball_zero {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) : ball H v 0 = {v}

theorem Complexity.Frontier.Gaussian.ball_subset_ball_of_adj {W : Type} [Fintype W] (H : SimpleGraph W) {u v : W} (h : H.Adj u v) (R : ℕ) : ball H v R ⊆ ball H u (R + 1)

The ball around a neighbour lies in the ball of one larger radius.

theorem Complexity.Frontier.Gaussian.mem_ball_of_not_disjoint {W : Type} [Fintype W] (H : SimpleGraph W) {a b : W} {r r' : ℕ} (h : ¬Disjoint (ball H a r) (ball H b r')) : b ∈ ball H a (r + r')

Overlapping balls have centres within the sum of their radii.

theorem Complexity.Frontier.Gaussian.kernel_eq_zero_of_notMem_ball {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {v z : W} (h : z ∉ ball H v R) : kernel H q R v z = 0

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

theorem Complexity.Frontier.Gaussian.kernel_of_mem_ball {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {v z : W} (h : z ∈ ball H v R) : kernel H q R v z = q ^ H.dist v z

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

theorem Complexity.Frontier.Gaussian.one_le_sum_kernel_sq {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} (R : ℕ) (v : W) : 1 ≤ ∑ z : W, kernel H q R v z ^ 2

Every kernel row has squared norm at least one.

theorem Complexity.Frontier.Gaussian.sum_unitKernel_sq {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (v : W) : ∑ z : W, unitKernel H q R v z ^ 2 = 1

The unit kernel row has norm one.

theorem Complexity.Frontier.Gaussian.unitKernel_eq_zero_of_notMem_ball {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {v z : W} (h : z ∉ ball H v R) : unitKernel H q R v z = 0

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

theorem Complexity.Frontier.Gaussian.unitKernel_nonneg {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) (v z : W) : 0 ≤ unitKernel H q R v z

The unit kernel is nonnegative for a nonnegative ratio.

theorem Complexity.Frontier.Gaussian.card_sphere_succ_le_degree {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {D : ℕ} (degree : ∀ (v : W), H.degree v ≤ D) (v : W) (d : ℕ) : (sphere H v (d + 1)).card ≤ D * (D - 1) ^ d

In maximum degree D, the sphere of radius d + 1 has at most D * (D - 1) ^ d vertices.

theorem Complexity.Frontier.Gaussian.card_sphere_succ_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (v : W) (d : ℕ) : (sphere H v (d + 1)).card ≤ 3 * 2 ^ d

theorem Complexity.Frontier.Gaussian.card_sphere_le_degree {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {D : ℕ} (hD : 2 ≤ D) (degree : ∀ (v : W), H.degree v ≤ D) (v : W) (d : ℕ) : (sphere H v d).card ≤ D * (D - 1) ^ d

Sphere growth in any fixed maximum degree.

theorem Complexity.Frontier.Gaussian.card_ball_le_degree {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {D : ℕ} (hD : 2 ≤ D) (degree : ∀ (v : W), H.degree v ≤ D) (v : W) (r : ℕ) : (ball H v r).card ≤ D ^ (r + 1)

A convenient locality bound; sharp ball growth is unnecessary for concentration.

theorem Complexity.Frontier.Gaussian.card_sphere_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (v : W) (d : ℕ) : (sphere H v d).card ≤ 3 * 2 ^ d

In a graph of maximum degree three, the sphere of radius d has at most 3 * 2 ^ d vertices.

theorem Complexity.Frontier.Gaussian.card_ball_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (v : W) (r : ℕ) : (ball H v r).card ≤ 3 * 2 ^ (r + 1)

In a graph of maximum degree three, the ball of radius r has at most 3 * 2 ^ (r + 1) vertices.

theorem Complexity.Frontier.Gaussian.sum_kernel_mul_ge_degree {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {D : ℕ} (hD : 2 ≤ D) (degree : ∀ (v : W), H.degree v ≤ D) (q : ℝ) (R : ℕ) {u v : W} (huv : H.Adj u v) : 2 * q / (1 + q ^ 2) * (∑ z : W, kernel H q R u z ^ 2 + ∑ z : W, kernel H q R v z ^ 2) / 2 - ↑D * (↑(D - 1) * q ^ 2) ^ R ≤ ∑ z : W, kernel H q R u z * kernel H q R v z

Pointwise correlation inequality, summed. For adjacent vertices the kernel rows have inner product at least κ times the mean of their squared norms, up to the truncation boundary, where κ = 2q/(1+q^2).

theorem Complexity.Frontier.Gaussian.sum_kernel_mul_ge {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (q : ℝ) (R : ℕ) {u v : W} (huv : H.Adj u v) : 2 * q / (1 + q ^ 2) * (∑ z : W, kernel H q R u z ^ 2 + ∑ z : W, kernel H q R v z ^ 2) / 2 - 3 * (2 * q ^ 2) ^ R ≤ ∑ z : W, kernel H q R u z * kernel H q R v z

theorem Complexity.Frontier.Gaussian.sum_unitKernel_mul_ge_degree {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {D : ℕ} (hD : 2 ≤ D) (degree : ∀ (v : W), H.degree v ≤ D) {q : ℝ} (hq0 : 0 ≤ q) (R : ℕ) {u v : W} (huv : H.Adj u v) : 2 * q / (1 + q ^ 2) - ↑D * (↑(D - 1) * q ^ 2) ^ R ≤ ∑ z : W, unitKernel H q R u z * unitKernel H q R v z

Correlation of adjacent rows. For a nonnegative ratio q, the unit kernel rows of adjacent vertices have inner product at least 2q/(1+q^2) - D ((D-1)q^2)^R.

theorem Complexity.Frontier.Gaussian.sum_unitKernel_mul_ge {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) {q : ℝ} (hq0 : 0 ≤ q) (R : ℕ) {u v : W} (huv : H.Adj u v) : 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R ≤ ∑ z : W, unitKernel H q R u z * unitKernel H q R v z