Shared estimates of the Gaussian layouts

The Gaussian layouts score the vertices, or the edges, of a multigraph G by inner products of vectors built from the unit kernel rows of its underlying simple graph H (Cslib.Circuits.Frontier.Gaussian.unitKernelRow) with a sample ω of independent standard Gaussians, one per vertex. This file collects the estimates shared by the vertex scores and the edge scores.

• Locality. The scores at a vertex v depend only on the coordinates of ω in the closed ball of radius R + 1 around v (closedBall). In maximum degree d such a ball meets at most vertexOverlap d R of the balls around the vertices, and as many around the sources of the edges.
• Concentration. The number of local events that occur deviates from its mean by c with probability O(|events| / c ^ 2) (measureReal_deviation_le).
• Projections. The product of standard Gaussians on V → ℝ is carried to the standard Gaussian measure of EuclideanSpace ℝ V, so a unit projection lands in a window of width δ with probability at most δ / √(2π) (measureReal_window_le), beyond T with probability at most 1 / T ^ 2 (measureReal_le_abs_le), and two projections of equal norm are separated by a threshold with probability at most their angle over π (measureReal_mem_uIoc_le, Sheppard's bound [She99]).
• Correlations. In maximum degree d, the unit kernel rows of adjacent vertices have inner product at least 2 q / (1 + q ^ 2) - d ((d - 1) q ^ 2) ^ R, and every value below 2 √(d - 1) / d (vertexCorrelation) is reached (exists_decay_radius_degree).

Main definitions

• Cslib.Circuits.Frontier.Gaussian.closedBall: the closed ball of a simple graph.
• Cslib.Circuits.Frontier.Gaussian.vertexOverlap: the overlap bound of the balls.
• Cslib.Circuits.Frontier.Gaussian.deviation: the event that a count of events deviates from its mean.
• Cslib.Circuits.Frontier.Gaussian.vertexCorrelation: the limiting correlation of adjacent kernel rows in maximum degree d.

Main results

• Cslib.Circuits.Frontier.Gaussian.closedBall_tgt_subset: the ends of an edge are within distance one.
• Cslib.Circuits.Frontier.Gaussian.card_not_disjoint_closedBall_le, Cslib.Circuits.Frontier.Gaussian.card_not_disjoint_closedBall_src_le: overlapping balls.
• Cslib.Circuits.Frontier.Gaussian.measureReal_deviation_le: concentration of counts of local events.
• Cslib.Circuits.Frontier.Gaussian.measureReal_window_le, Cslib.Circuits.Frontier.Gaussian.measureReal_le_abs_le, Cslib.Circuits.Frontier.Gaussian.measureReal_mem_uIoc_le: windows, tails and crossings.
• Cslib.Circuits.Frontier.Gaussian.le_inner_unitKernelRow_src_tgt: the correlation of the rows at the ends of an edge.
• Cslib.Circuits.Frontier.Gaussian.exists_decay_radius_degree: every correlation below vertexCorrelation d is reached.

References

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

def Cslib.Circuits.Frontier.Gaussian.closedBall {V : Type u_1} (H : SimpleGraph V) (v : V) (r : ℕ) : Set V

The closed ball of radius r around v in a simple graph, for the extended distance.

def Cslib.Circuits.Frontier.Gaussian.vertexOverlap (d R : ℕ) : ℕ

The number of closed balls of radius R + 1 that may meet a given one, around the vertices or around the sources of the edges of a multigraph of maximum degree d.

Locality

theorem Cslib.Circuits.Frontier.Gaussian.closedBall_tgt_subset {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (e : E) (r : ℕ) : closedBall G.toSimpleGraph (G.tgt e) r ⊆ closedBall G.toSimpleGraph (G.src e) (r + 1)

The closed ball of radius r around the target of an edge lies in the closed ball of radius r + 1 around its source.

theorem Cslib.Circuits.Frontier.Gaussian.card_not_disjoint_closedBall_le {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} [Finite E] {d : ℕ} (hdeg : G.MaxDegreeLE d) (hd : 1 ≤ d) (R : ℕ) (v : V) : {w : V | ¬Disjoint (closedBall G.toSimpleGraph v (R + 1)) (closedBall G.toSimpleGraph w (R + 1))}.card ≤ vertexOverlap d R

In a multigraph of maximum degree d ≥ 1, a closed ball of radius R + 1 meets at most vertexOverlap d R of the closed balls of radius R + 1 around the vertices.

theorem Cslib.Circuits.Frontier.Gaussian.card_not_disjoint_closedBall_src_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] {d : ℕ} [Finite V] [Fintype E] (hdeg : G.MaxDegreeLE d) (R : ℕ) (e : E) : {l : E | ¬Disjoint (closedBall G.toSimpleGraph (G.src e) (R + 1)) (closedBall G.toSimpleGraph (G.src l) (R + 1))}.card ≤ vertexOverlap d R

In a multigraph of maximum degree d, the closed ball of radius R + 1 around the source of an edge meets at most vertexOverlap d R of the closed balls of radius R + 1 around the sources of the edges.

Deviations of counts

theorem Cslib.Circuits.Frontier.Gaussian.ncard_eq_sum_indicator {Ω : Type u_1} {κ : Type u_2} [Fintype κ] (A : κ → Set Ω) (ω : Ω) : ↑{k : κ | ω ∈ A k}.ncard = ∑ k : κ, (A k).indicator 1 ω

The number of events that occur is the sum of their indicators.

theorem Cslib.Circuits.Frontier.Gaussian.ncard_lt_of_not_le_abs {Ω : Type u_1} {κ : Type u_2} [Fintype κ] {A : κ → Set Ω} {ω : Ω} {m c : ℝ} (h : ¬c ≤ |∑ k : κ, (A k).indicator 1 ω - m|) : ↑{k : κ | ω ∈ A k}.ncard < m + c

Outside the event that the number of events that occur deviates from m by at least c, this number is below m + c.

theorem Cslib.Circuits.Frontier.Gaussian.exists_sample_of_grid_bounds {Ω : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A B : ℕ → Set Ω} {C D : Set Ω} {a b c d : ℝ} {M : ℕ} (hA : ∀ i < M, P.real (A i) ≤ a) (hB : ∀ i < M, P.real (B i) ≤ b) (hC : P.real C ≤ c) (hD : P.real D ≤ d) (hsmall : ↑M * (a + b) + c + d < 1) : ∃ (ω : Ω), (∀ i < M, ω ∉ A i ∧ ω ∉ B i) ∧ ω ∉ C ∧ ω ∉ D

Simultaneously avoid two families of grid events and both tail events when their probability bounds sum to less than one.

def Cslib.Circuits.Frontier.Gaussian.deviation {κ : Type u_2} [Fintype κ] {V : Type u_3} [Fintype V] (A : κ → Set (V → ℝ)) (c : ℝ) : Set (V → ℝ)

The event that the number of the events A k that occur deviates from its mean under the product of standard Gaussians by at least c.

theorem Cslib.Circuits.Frontier.Gaussian.ncard_lt_of_notMem_deviation {κ : Type u_2} [Fintype κ] {V : Type u_3} [Fintype V] {A : κ → Set (V → ℝ)} {c : ℝ} {ω : V → ℝ} (h : ω ∉ deviation A c) : ↑{k : κ | ω ∈ A k}.ncard < ∑ k : κ, (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (A k) + c

Outside the deviation event, the number of events that occur is below its mean plus c.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_deviation_le {κ : Type u_2} [Fintype κ] {V : Type u_3} [Fintype V] {A : κ → Set (V → ℝ)} (hA : ∀ (k : κ), MeasurableSet (A k)) (S : κ → Set V) (hAS : ∀ (k : κ), DependsOn (fun (x : V → ℝ) => x ∈ A k) (S k)) {D : ℕ} (hD : ∀ (k : κ), {l : κ | ¬Disjoint (S k) (S l)}.card ≤ D) {c : ℝ} (hc : 0 < c) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (deviation A c) ≤ ↑(Fintype.card κ) * ↑D / c ^ 2

Concentration of local events. Under the product of standard Gaussians, if each event A k depends only on the coordinates in S k, and each S k meets at most D of the sets S l, then the number of events that occur deviates from its mean by at least c > 0 with probability at most |κ| D / c ^ 2.

Projections of the sample

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_pi_eq {V : Type u_1} [Fintype V] {s : Set (EuclideanSpace ℝ V)} (hs : MeasurableSet s) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real {ω : V → ℝ | WithLp.toLp 2 ω ∈ s} = (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ V)).real s

The product of standard Gaussians on V → ℝ carries an event about inner products to the same event under the standard Gaussian measure of EuclideanSpace ℝ V.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_window_le {V : Type u_1} [Fintype V] {y : EuclideanSpace ℝ V} (hy : ‖y‖ = 1) (a : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real {ω : V → ℝ | a ≤ inner ℝ y (WithLp.toLp 2 ω) ∧ inner ℝ y (WithLp.toLp 2 ω) < a + δ} ≤ δ / √(2 * Real.pi)

Window bound. A unit projection of the sample lands in a window of width δ ≥ 0 with probability at most δ / √(2π).

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_le_abs_le {V : Type u_1} [Fintype V] {y : EuclideanSpace ℝ V} (hy : ‖y‖ = 1) {T : ℝ} (hT : 0 < T) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real {ω : V → ℝ | T ≤ |inner ℝ y (WithLp.toLp 2 ω)|} ≤ 1 / T ^ 2

Tail bound. A unit projection of the sample has absolute value at least T > 0 with probability at most 1 / T ^ 2.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_mem_uIoc_le {V : Type u_1} [Fintype V] {y y' : EuclideanSpace ℝ V} (h : ‖y‖ = ‖y'‖) (t : ℝ) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real {ω : V → ℝ | t ∈ Set.uIoc (inner ℝ y (WithLp.toLp 2 ω)) (inner ℝ y' (WithLp.toLp 2 ω))} ≤ InnerProductGeometry.angle y y' / Real.pi

Sheppard's bound for the sample. Two projections of the sample onto vectors of equal norm are separated by a threshold with probability at most their angle over π.

theorem Cslib.Circuits.Frontier.Gaussian.inner_toLp_congr {V : Type u_1} [Fintype V] {y : EuclideanSpace ℝ V} {S : Set V} (hy : ∀ z ∉ S, y.ofLp z = 0) {ω ω' : V → ℝ} (h : ∀ z ∈ S, ω z = ω' z) : inner ℝ y (WithLp.toLp 2 ω) = inner ℝ y (WithLp.toLp 2 ω')

An inner product with a vector y depends only on the coordinates where y is nonzero.

Correlations of adjacent rows

theorem Cslib.Circuits.Frontier.Gaussian.le_inner_unitKernelRow_src_tgt {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} [Finite E] (hloop : G.Loopless) {d : ℕ} (hd : 2 ≤ d) (hdeg : G.MaxDegreeLE d) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) (e : E) : 2 * q / (1 + q ^ 2) - ↑d * ((↑d - 1) * q ^ 2) ^ R ≤ inner ℝ (unitKernelRow G.toSimpleGraph q R (G.src e)) (unitKernelRow G.toSimpleGraph q R (G.tgt e))

Adjacent rows are correlated. In a loopless multigraph of maximum degree d ≥ 2, the unit kernel rows of the ends of an edge, in the underlying simple graph, have inner product at least 2 q / (1 + q ^ 2) - d ((d - 1) q ^ 2) ^ R.

theorem Cslib.Circuits.Frontier.Gaussian.continuous_correlation : Continuous fun (q : ℝ) => 2 * q / (1 + q ^ 2)

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

The limiting correlation 2 √(d - 1) / d of the kernel rows of adjacent vertices in maximum degree d: the neighbour correlation of Gaussian waves on the d-regular tree.

theorem Cslib.Circuits.Frontier.Gaussian.vertexCorrelation_pos {d : ℕ} (hd : 2 ≤ d) : 0 < vertexCorrelation d

theorem Cslib.Circuits.Frontier.Gaussian.exists_decay_radius_degree {d : ℕ} (hd : 2 ≤ d) {ρ : ℝ} (hρ : ρ < vertexCorrelation d) : ∃ (q : ℝ) (R : ℕ), 0 ≤ q ∧ ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * ((↑d - 1) * q ^ 2) ^ R

Decay rate and radius. In maximum degree d ≥ 2, every correlation below vertexCorrelation d is met by the truncated kernel bound for some decay rate q ≥ 0 and some radius R.