Gaussian edge scores and their locality

Let G be a loopless multigraph of maximum degree three, with underlying simple graph H. Give each edge e the unit vector y_e in the direction of x_u + x_v, where x_u and x_v are the unit kernel rows of its ends in H (Cslib.Circuits.Frontier.Gaussian.edgeVector). Its score at a sample ω is ⟪y_e, ω⟫ (Cslib.Circuits.Frontier.Gaussian.edgeScore).

If the rows of adjacent vertices have inner product ρ, the edge vector has inner product √((1 + ρ)/2) with the row of either end: the sum of two unit vectors with inner product ρ has norm 2 √((1 + ρ)/2). The edge vectors at a vertex v vanish outside the closed ball of radius R + 1 around v, so the scores of the edges at v depend only on the coordinates of the sample in that ball (Cslib.Circuits.Frontier.Gaussian.edgeScore_congr).

Main definitions

• Cslib.Circuits.Frontier.Gaussian.edgeVector: the unit vector of an edge.
• Cslib.Circuits.Frontier.Gaussian.edgeScore: the Gaussian score of an edge.

Main results

• Cslib.Circuits.Frontier.Gaussian.norm_edgeVector: edge vectors are unit vectors.
• Cslib.Circuits.Frontier.Gaussian.le_inner_edgeVector: the edge vectors at v are close to the row of v.
• Cslib.Circuits.Frontier.Gaussian.edgeScore_congr: locality of the scores.

Normalized sums of unit vectors

Edge vectors and scores

noncomputable def Cslib.Circuits.Frontier.Gaussian.edgeVector {V : Type u_1} {E : Type u_2} [Fintype V] (G : Multigraph V E) (q : ℝ) (R : ℕ) (e : E) : EuclideanSpace ℝ V

The unit vector of an edge: the sum of the unit kernel rows of its ends, in the underlying simple graph, divided by its norm.

noncomputable def Cslib.Circuits.Frontier.Gaussian.edgeScore {V : Type u_1} {E : Type u_2} [Fintype V] (G : Multigraph V E) (q : ℝ) (R : ℕ) (ω : V → ℝ) (e : E) : ℝ

The Gaussian score of an edge at a sample ω: the inner product of its unit vector with ω.

theorem Cslib.Circuits.Frontier.Gaussian.measurable_edgeScore {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) (e : E) : Measurable fun (ω : V → ℝ) => edgeScore G q R ω e

theorem Cslib.Circuits.Frontier.Gaussian.norm_edgeVector {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {ρ₀ : ℝ} [Finite E] (hloop : G.Loopless) (hdeg : G.MaxDegreeLE 3) (hq : 0 ≤ q) (hρ₀ : -1 < ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) (e : E) : ‖edgeVector G q R e‖ = 1

Edge vectors are unit vectors, when adjacent rows have inner product at least ρ₀ > -1.

theorem Cslib.Circuits.Frontier.Gaussian.le_inner_edgeVector {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {ρ₀ : ℝ} [Finite E] (hloop : G.Loopless) (hdeg : G.MaxDegreeLE 3) (hq : 0 ≤ q) (hρ₀ : 0 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) {v : V} {e : E} (he : e ∈ G.incidenceSet v) : √((1 + ρ₀) / 2) ≤ inner ℝ (edgeVector G q R e) (unitKernelRow G.toSimpleGraph q R v)

Edge vectors are close to the rows of their ends. If adjacent rows have inner product at least ρ₀ ≥ 0, an edge vector has inner product at least √((1 + ρ₀)/2) with the row of either end.

Locality

theorem Cslib.Circuits.Frontier.Gaussian.edgeVector_apply_eq_zero {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {v : V} {e : E} (he : e ∈ G.incidenceSet v) {z : V} (hz : z ∉ closedBall G.toSimpleGraph v (R + 1)) : (edgeVector G q R e).ofLp z = 0

The edge vectors at v vanish outside the closed ball of radius R + 1 around v.

theorem Cslib.Circuits.Frontier.Gaussian.edgeScore_congr {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {v : V} {e : E} (he : e ∈ G.incidenceSet v) {ω ω' : V → ℝ} (h : ∀ z ∈ closedBall G.toSimpleGraph v (R + 1), ω z = ω' z) : edgeScore G q R ω e = edgeScore G q R ω' e

Locality. The scores of the edges at v depend only on the coordinates of the sample in the closed ball of radius R + 1 around v.