Correlation of truncated distance kernels

This file bounds the truncated distance kernel of Gaussian.Kernel.Defs on a graph of maximum degree three.

• card_sphere_le and card_ball_le: spheres and balls grow at most like 3 * 2 ^ d, since a vertex at positive distance d has a neighbour at distance d - 1 and hence at most two neighbours at distance d + 1.
• sum_kernel_mul_ge: for adjacent u and v, the kernel rows have inner product at least κ = 2q / (1 + q²) times the mean of their squared norms, up to 3 * (2 * q ^ 2) ^ R contributed by the truncation spheres.
• sum_unitKernel_mul_ge: for 0 ≤ q, the unit kernel rows of adjacent vertices have inner product at least κ - 3 * (2 * q ^ 2) ^ R.

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

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

@[simp]

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

theorem Algebraic.Cutwidth.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 Algebraic.Cutwidth.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 Algebraic.Cutwidth.Gaussian.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.sphere_zero {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) : sphere H v 0 = {v}

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

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

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

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

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

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

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

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²).

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

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