Gaussian vertex scores

Let G be a loopless multigraph of maximum degree d, with underlying simple graph H. Give each vertex v its unit kernel row x_v in H (Cslib.Circuits.Frontier.Gaussian.unitKernelRow): the normalized vector of distance weights q ^ dist(v, z), truncated at radius R. Draw a sample ω of independent standard Gaussians, one per vertex, and score each vertex by ⟪x_v, ω⟫ (Cslib.Circuits.Frontier.Gaussian.vertexScore). Sorting the vertices by score gives the layouts of the module Complexity.Computability.Circuit.Frontier.Layouts.MultiGaussian.

One edge. A threshold t crosses an edge when it separates the scores of its ends (Cslib.Circuits.Frontier.Gaussian.crossingEvent). The rows of the ends have inner product at least ρ, for any ρ below the truncated kernel bound 2 q / (1 + q ^ 2) - d ((d - 1) q ^ 2) ^ R, so by Sheppard's bound [She99] the edge is crossed with probability at most arccos ρ / π (Cslib.Circuits.Frontier.Gaussian.measureReal_crossingEvent_le).

Locality. A score depends only on the coordinates of ω in the closed ball of radius R around its vertex, so the events about the score of v, and the crossing of an edge, depend only on the closed ball of radius R + 1 around v, or around the source of the edge.

The limit. As q increases to 1/√(d - 1) and R grows, the adjacent correlation tends to 2 √(d - 1) / d (Cslib.Circuits.Frontier.Gaussian.vertexCorrelation), the neighbour correlation of Gaussian waves on the d-regular tree. So the crossing probability of an edge tends to vertexCoefficient d = arccos (2 √(d - 1) / d) / π.

Main definitions

• Cslib.Circuits.Frontier.Gaussian.vertexScore: the Gaussian score of a vertex.
• Cslib.Circuits.Frontier.Gaussian.vertexEvent: an event about the score of a vertex.
• Cslib.Circuits.Frontier.Gaussian.crossingEvent: a threshold separates the scores of the ends of an edge.
• Cslib.Circuits.Frontier.Gaussian.vertexCoefficient: the limiting crossing probability arccos (2 √(d - 1) / d) / π.

Main results

• Cslib.Circuits.Frontier.Gaussian.dependsOn_vertexEvent, Cslib.Circuits.Frontier.Gaussian.dependsOn_crossingEvent: locality.
• Cslib.Circuits.Frontier.Gaussian.measureReal_crossingEvent_le: the crossing probability of an edge.

References

• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation

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

The Gaussian score ⟪x_v, ω⟫ of a vertex: the inner product of its unit kernel row, in the underlying simple graph, with the sample.

def Cslib.Circuits.Frontier.Gaussian.vertexEvent {V : Type u_1} {E : Type u_2} [Fintype V] (G : Multigraph V E) (q : ℝ) (R : ℕ) (p : ℝ → Prop) (v : V) : Set (V → ℝ)

The event that the score of v satisfies p.

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

The event that the threshold t separates the scores of the ends of an edge.

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

theorem Cslib.Circuits.Frontier.Gaussian.measurableSet_vertexEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) {p : ℝ → Prop} (hp : MeasurableSet {x : ℝ | p x}) (v : V) : MeasurableSet (vertexEvent G q R p v)

theorem Cslib.Circuits.Frontier.Gaussian.measurableSet_crossingEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) (t : ℝ) (e : E) : MeasurableSet (crossingEvent G q R t e)

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

The score of v depends only on the coordinates of the sample in the closed ball of radius R around v.

theorem Cslib.Circuits.Frontier.Gaussian.dependsOn_vertexEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) (p : ℝ → Prop) (v : V) : DependsOn (fun (x : V → ℝ) => x ∈ vertexEvent G q R p v) (closedBall G.toSimpleGraph v (R + 1))

Locality. An event about the score of v depends only on the coordinates of the sample in the closed ball of radius R + 1 around v.

theorem Cslib.Circuits.Frontier.Gaussian.dependsOn_crossingEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) (t : ℝ) (e : E) : DependsOn (fun (x : V → ℝ) => x ∈ crossingEvent G q R t e) (closedBall G.toSimpleGraph (G.src e) (R + 1))

Locality. Whether a threshold crosses an edge depends only on the coordinates of the sample in the closed ball of radius R + 1 around its source.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_crossingEvent_le {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} [Finite E] (hloop : G.Loopless) {d : ℕ} (hd : 2 ≤ d) (hdeg : G.MaxDegreeLE d) (hq : 0 ≤ q) (R : ℕ) {ρ : ℝ} (hρ : ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * ((↑d - 1) * q ^ 2) ^ R) (t : ℝ) (e : E) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (crossingEvent G q R t e) ≤ Real.arccos ρ / Real.pi

One edge. In a loopless multigraph of maximum degree d ≥ 2, let ρ be at most the truncated kernel bound 2 q / (1 + q ^ 2) - d ((d - 1) q ^ 2) ^ R. A threshold crosses an edge with probability at most arccos ρ / π.

noncomputable def Cslib.Circuits.Frontier.Gaussian.vertexCoefficient (d : ℕ) : ℝ

The limiting crossing probability of an edge under Gaussian vertex scores in maximum degree d: arccos (2 √(d - 1) / d) / π.