Distance-kernel internals

Proofs of the sphere growth bounds and of the correlation inequality for the truncated distance kernel.

A vertex at distance d + 1 from v has a neighbour at distance d: the penultimate vertex of a shortest walk. In a graph of maximum degree three, a vertex at positive distance d therefore has at most two neighbours at distance d + 1, which gives |S_{d+1}(v)| ≤ 3 * 2 ^ d.

For adjacent u and v, the distances from u and v to any vertex differ by at most one. When both kernel values are nonzero they are equal or differ by the factor q, and x * y ≥ κ (x² + y²) / 2 with κ = 2q / (1 + q²). When exactly one is nonzero it lies on the truncation sphere of radius R.

theorem Algebraic.Cutwidth.Gaussian.Internal.edist_le_edist_add_one {W : Type} (H : SimpleGraph W) {u v : W} (huv : H.Adj u v) (z : W) : H.edist u z ≤ H.edist v z + 1

Adjacent vertices have extended distances to any vertex differing by at most one.

theorem Algebraic.Cutwidth.Gaussian.Internal.edist_eq_dist_of_le {W : Type} (H : SimpleGraph W) {v z : W} {n : ℕ} (h : H.edist v z ≤ ↑n) : H.edist v z = ↑(H.dist v z)

A bounded extended distance is the cast of the natural distance.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_adj_edist_eq {W : Type} (H : SimpleGraph W) {v z : W} {k : ℕ} (h : H.edist v z = ↑(k + 1)) : ∃ (w : W), H.Adj w z ∧ H.edist v w = ↑k

A vertex at distance k + 1 has a neighbour at distance k.

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

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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.kappa_le_one (q : ℝ) : 2 * q / (1 + q ^ 2) ≤ 1

κ = 2q / (1 + q²) is at most one for every real q.

theorem Algebraic.Cutwidth.Gaussian.Internal.kappa_mul_sq_add_sq (q x : ℝ) : 2 * q / (1 + q ^ 2) * (x ^ 2 + (x * q) ^ 2) / 2 = x * (x * q)

Rows whose distances differ by one meet the correlation bound with equality.

theorem Algebraic.Cutwidth.Gaussian.Internal.kernel_defect_le {W : Type} (H : SimpleGraph W) {q : ℝ} (R : ℕ) {u v : W} (huv : H.Adj u v) (z : W) : 2 * q / (1 + q ^ 2) * (kernel H q R u z ^ 2 + kernel H q R v z ^ 2) / 2 - kernel H q R u z * kernel H q R v z ≤ (q ^ 2) ^ R / 2 * ((if H.edist u z = ↑R then 1 else 0) + if H.edist v z = ↑R then 1 else 0)

Pointwise defect. For adjacent u and v, the kernel values at z fall short of κ times their mean square only on the truncation spheres.

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

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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.sphere_subset_ball {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) (r : ℕ) : sphere H v r ⊆ ball H v r

theorem Algebraic.Cutwidth.Gaussian.Internal.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)

theorem Algebraic.Cutwidth.Gaussian.Internal.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')

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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.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

theorem Algebraic.Cutwidth.Gaussian.Internal.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

theorem Algebraic.Cutwidth.Gaussian.Internal.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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.sum_unitKernel_mul {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) : ∑ z : W, unitKernel H q R u z * unitKernel H q R v z = (∑ z : W, kernel H q R u z * kernel H q R v z) / (√(∑ z : W, kernel H q R u z ^ 2) * √(∑ z : W, kernel H q R v z ^ 2))

The unit kernel rows have inner product equal to the kernel inner product divided by both row norms.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_neighborFinset_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) {v w : W} {d : ℕ} (hw : H.edist v w = ↑(d + 1)) : {y ∈ H.neighborFinset w | H.edist v y = ↑(d + 1 + 1)}.card ≤ 2

A vertex at positive distance d + 1 has at most two neighbours at distance d + 2.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_sphere_one_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (v : W) : (sphere H v 1).card ≤ 3

theorem Algebraic.Cutwidth.Gaussian.Internal.card_sphere_succ_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 + 1)).card ≤ 2 * (sphere H v (d + 1)).card

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.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

theorem Algebraic.Cutwidth.Gaussian.Internal.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)

theorem Algebraic.Cutwidth.Gaussian.Internal.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

Kernel correlation.

theorem Algebraic.Cutwidth.Gaussian.Internal.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

Unit kernel correlation.