Gaussian layouts of cubic graphs

Every large simple cubic graph on h vertices has a layout whose prefixes are crossed by at most (p + ξ) h edges, where

p = (3/(2π)) arccos ((1 + 2√2)/4) ≈ 0.14035

is gaussianCoefficient (cubicLayoutBound_gaussian).

The random layout. Give each vertex v its unit kernel row x_v (Frontier.Gaussian.Kernel): the normalized vector of distance weights q ^ dist(v, z), truncated at radius R. Give each edge uv the unit vector y_uv in the direction of x_u + x_v. Draw a standard Gaussian vector ω and score each edge by ⟨y_e, ω⟩. List the vertices by the median of their three edge scores (Frontier.Layouts.Median).

One vertex. A vertex straddles a threshold when two of its edge scores fall on opposite sides. The three edge vectors at v have correlation at least √((1 + ρ)/2) with x_v, where ρ bounds the correlation of adjacent rows; by Sheppard's bound a pair with correlation ρ' is separated with probability at most arccos ρ' / π, and the star inequality (Frontier.Gaussian.Star) bounds the probability that v straddles any fixed threshold by (3/(2π)) arccos ((1 + 3ρ)/4) (measureReal_straddleEvent_le).

All thresholds at once. Each event depends only on the coordinates of ω in a ball of bounded radius, so each count of events has variance O(h) and is within ε h of its mean with probability 1 - O(1/h) (Frontier.Gaussian.SecondMoment). For large h one sample keeps the straddling counts at a grid of thresholds, the window counts between them, and the tails near their means (exists_good_sample); the median layout of that sample has every prefix cut at most (p_ρ + O(δ) + O(ε) + O(1/T^2)) h.

The limit. As q increases to 1/√2 and R grows, the adjacent correlation tends to 2√2/3, the neighbour correlation of Gaussian waves on the 3-regular tree, and (1 + 3 · 2√2/3)/4 = (1 + 2√2)/4.

noncomputable def Complexity.Frontier.Gaussian.gaussianCoefficient : ℝ

The cubic layout coefficient of Gaussian edge scores, (3/(2π)) arccos ((1 + 2√2)/4).

Equations

• Complexity.Frontier.Gaussian.gaussianCoefficient = 3 / (2 * Real.pi) * Real.arccos ((1 + 2 * √2) / 4)

Edge vectors and scores

noncomputable def Complexity.Frontier.Gaussian.pairNormSq {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) : ℝ

The squared norm of the sum of two unit kernel rows.

Equations

• Complexity.Frontier.Gaussian.pairNormSq H q R u v = ∑ z : W, (Complexity.Frontier.Gaussian.unitKernel H q R u z + Complexity.Frontier.Gaussian.unitKernel H q R v z) ^ 2

theorem Complexity.Frontier.Gaussian.pairNormSq_comm {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) : pairNormSq H q R u v = pairNormSq H q R v u

theorem Complexity.Frontier.Gaussian.pairNormSq_eq {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) : pairNormSq H q R u v = 2 + 2 * ∑ z : W, unitKernel H q R u z * unitKernel H q R v z

noncomputable def Complexity.Frontier.Gaussian.edgeVector {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) : Sym2 W → W → ℝ

The unit vector of an edge: the normalized sum of the kernel rows of its endpoints.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.Frontier.Gaussian.edgeVector_mk {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v z : W) : edgeVector H q R s(u, v) z = (unitKernel H q R u z + unitKernel H q R v z) / √(pairNormSq H q R u v)

noncomputable def Complexity.Frontier.Gaussian.edgeScore {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (ω : W → ℝ) (e : Sym2 W) : ℝ

The Gaussian score of an edge at the sample ω.

Equations

• Complexity.Frontier.Gaussian.edgeScore H q R ω e = Complexity.Frontier.Gaussian.form (Complexity.Frontier.Gaussian.edgeVector H q R e) ω

theorem Complexity.Frontier.Gaussian.measurable_edgeScore {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (e : Sym2 W) : Measurable fun (ω : W → ℝ) => edgeScore H q R ω e

theorem Complexity.Frontier.Gaussian.sum_edgeVector_sq {W : Type} [Fintype W] {H : SimpleGraph W} {q : ℝ} {R : ℕ} {u v : W} (hpos : 0 < pairNormSq H q R u v) : ∑ z : W, edgeVector H q R s(u, v) z ^ 2 = 1

theorem Complexity.Frontier.Gaussian.sum_edgeVector_mul {W : Type} [Fintype W] {H : SimpleGraph W} {q : ℝ} {R : ℕ} {u v : W} (hpos : 0 < pairNormSq H q R u v) : ∑ z : W, edgeVector H q R s(u, v) z * unitKernel H q R v z = √((1 + ∑ z : W, unitKernel H q R u z * unitKernel H q R v z) / 2)

The inner product of an edge vector with the row of an endpoint is √((1 + ρ)/2), where ρ is the correlation of the two endpoint rows.

Locality

theorem Complexity.Frontier.Gaussian.form_congr {ι : Type} [Fintype ι] {α : ι → ℝ} {S : Finset ι} (hα : ∀ i ∉ S, α i = 0) {ω ω' : ι → ℝ} (h : ∀ i ∈ S, ω i = ω' i) : form α ω = form α ω'

A form depends only on the coordinates where its coefficients are nonzero.

noncomputable def Complexity.Frontier.Gaussian.edgeSupport {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (R : ℕ) : Sym2 W → Finset W

The coordinates on which the score of an edge depends: the kernel balls of its endpoints.

Equations

• Complexity.Frontier.Gaussian.edgeSupport H R = Sym2.lift ⟨fun (u v : W) => Complexity.Frontier.Gaussian.ball H u R ∪ Complexity.Frontier.Gaussian.ball H v R, ⋯⟩

@[simp]

theorem Complexity.Frontier.Gaussian.edgeSupport_mk {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (R : ℕ) (u v : W) : edgeSupport H R s(u, v) = ball H u R ∪ ball H v R

theorem Complexity.Frontier.Gaussian.edgeScore_congr_of_eq_zero {W : Type} [Fintype W] {H : SimpleGraph W} {q : ℝ} {R : ℕ} {e : Sym2 W} {S : Finset W} (hS : ∀ z ∉ S, edgeVector H q R e z = 0) {ω ω' : W → ℝ} (h : ∀ i ∈ S, ω i = ω' i) : edgeScore H q R ω e = edgeScore H q R ω' e

theorem Complexity.Frontier.Gaussian.edgeScore_congr {W : Type} [Fintype W] [DecidableEq W] {H : SimpleGraph W} {q : ℝ} {R : ℕ} {e : Sym2 W} {S : Finset W} (hS : edgeSupport H R e ⊆ S) {ω ω' : W → ℝ} (h : ∀ i ∈ S, ω i = ω' i) : edgeScore H q R ω e = edgeScore H q R ω' e

theorem Complexity.Frontier.Gaussian.edgeSupport_subset_ball {W : Type} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] {R : ℕ} {v : W} {e : Sym2 W} (he : e ∈ H.incidenceFinset v) : edgeSupport H R e ⊆ ball H v (R + 1)

The supports of the edges at v lie in the ball of radius R + 1 around v.

def Complexity.Frontier.Gaussian.overlapBound (R : ℕ) : ℕ

The number of supports that may meet a given one, in a graph of maximum degree three.

Equations

• Complexity.Frontier.Gaussian.overlapBound R = 9 * 2 ^ (2 * R + 2)

theorem Complexity.Frontier.Gaussian.card_filter_not_disjoint_edgeSupport_le {W : Type} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (R : ℕ) {e : Sym2 W} (he : e ∈ H.edgeFinset) : {l ∈ H.edgeFinset | ¬Disjoint (edgeSupport H R e) (edgeSupport H R l)}.card ≤ overlapBound R

Boundedly many edge supports meet that of a given edge.

theorem Complexity.Frontier.Gaussian.card_filter_not_disjoint_ball_le {W : Type} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (R : ℕ) (v : W) : {w : W | ¬Disjoint (ball H v R) (ball H w R)}.card ≤ overlapBound R

Boundedly many balls of radius R meet a given one.

The straddling probability of one vertex

noncomputable def Complexity.Frontier.Gaussian.straddleBound (ρ₀ : ℝ) : ℝ

The probability bound for straddling when adjacent kernel rows have correlation at least ρ₀.

Equations

• Complexity.Frontier.Gaussian.straddleBound ρ₀ = 3 / (2 * Real.pi) * Real.arccos ((1 + 3 * ρ₀) / 4)

def Complexity.Frontier.Gaussian.straddleEvent {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℝ) (R : ℕ) (t : ℝ) (v : W) : Set (W → ℝ)

The event that the edge scores at v straddle the threshold t.

Equations

• Complexity.Frontier.Gaussian.straddleEvent H q R t v = {ω : W → ℝ | Complexity.Frontier.EdgeStraddles H (Complexity.Frontier.Gaussian.edgeScore H q R ω) t v}

@[instance_reducible]

noncomputable instance Complexity.Frontier.Gaussian.instDecidableBetween (t x y : ℝ) : Decidable (Between t x y)

Equations

• Complexity.Frontier.Gaussian.instDecidableBetween t x y = id inferInstance

theorem Complexity.Frontier.Gaussian.edgeVector_star {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) {q : ℝ} (hq0 : 0 ≤ q) {R : ℕ} {ρ₀ : ℝ} (hρ₀ : -1 < ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) (v : W) {e : Sym2 W} (he : e ∈ H.incidenceFinset v) : ∑ z : W, edgeVector H q R e z ^ 2 = 1 ∧ √((1 + ρ₀) / 2) ≤ ∑ z : W, edgeVector H q R e z * unitKernel H q R v z

The edge vectors at v are unit vectors with correlation at least √((1 + ρ₀)/2) with the row of v.

theorem Complexity.Frontier.Gaussian.four_le_between_pairs {t p q r : ℝ} (hlt : p < t ∨ q < t ∨ r < t) (hge : t ≤ p ∨ t ≤ q ∨ t ≤ r) : 4 ≤ ((if Between t p q then 1 else 0) + if Between t p r then 1 else 0) + (((if Between t q p then 1 else 0) + if Between t q r then 1 else 0) + ((if Between t r p then 1 else 0) + if Between t r q then 1 else 0))

Three reals on both sides of a threshold give four separated ordered pairs.

theorem Complexity.Frontier.Gaussian.indicator_edgeStraddles_le {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] [DecidableEq W] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) (t : ℝ) (v : W) : (if EdgeStraddles H score t v then 1 else 0) ≤ 1 / 4 * ∑ e ∈ H.incidenceFinset v, ∑ e' ∈ (H.incidenceFinset v).erase e, if Between t (score e) (score e') then 1 else 0

A straddling vertex of a cubic graph has at least four separated ordered pairs of edges.

theorem Complexity.Frontier.Gaussian.measurableSet_between {Ω : Type} [MeasurableSpace Ω] {f g : Ω → ℝ} (hf : Measurable f) (hg : Measurable g) (t : ℝ) : MeasurableSet {ω : Ω | Between t (f ω) (g ω)}

theorem Complexity.Frontier.Gaussian.measurableSet_straddleEvent {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (q : ℝ) (R : ℕ) (t : ℝ) (v : W) : MeasurableSet (straddleEvent H q R t v)

theorem Complexity.Frontier.Gaussian.dependsOn_straddleEvent {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (q : ℝ) (R : ℕ) (t : ℝ) (v : W) : DependsOn (fun (x : W → ℝ) => x ∈ straddleEvent H q R t v) ↑(ball H v (R + 1))

Whether v straddles a threshold depends only on the ball of radius R + 1 around v.

theorem Complexity.Frontier.Gaussian.measureReal_straddleEvent_le {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) {q : ℝ} (hq0 : 0 ≤ q) {R : ℕ} {ρ₀ : ℝ} (hρ₀ : 17 / 32 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) (t : ℝ) (v : W) : (gaussPi W).real (straddleEvent H q R t v) ≤ straddleBound ρ₀

Straddling probability. If adjacent kernel rows have correlation at least ρ₀ ≥ 17/32, a vertex straddles any fixed threshold with probability at most straddleBound ρ₀.

A good sample

theorem Complexity.Frontier.Gaussian.card_edgeFinset_of_regular {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) : ↑H.edgeFinset.card = 3 / 2 * ↑(Fintype.card W)

def Complexity.Frontier.Gaussian.deviation {W : Type} [Fintype W] {κ : Type} (F : Finset κ) (A : κ → Set (W → ℝ)) (c : ℝ) : Set (W → ℝ)

The event that a count of events deviates from its mean by at least c.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.Gaussian.lt_of_notMem_deviation {W : Type} [Fintype W] {κ : Type} {F : Finset κ} {A : κ → Set (W → ℝ)} {c : ℝ} {ω : W → ℝ} (h : ω ∉ deviation F A c) : ∑ k ∈ F, (A k).indicator (fun (x : W → ℝ) => 1) ω < ∑ k ∈ F, (gaussPi W).real (A k) + c

theorem Complexity.Frontier.Gaussian.card_filter_le_sum_indicator {Ω κ : Type} (F : Finset κ) (A : κ → Set Ω) (ω : Ω) (p : κ → Prop) [DecidablePred p] (hp : ∀ k ∈ F, p k → ω ∈ A k) : ↑(Finset.filter p F).card ≤ ∑ k ∈ F, (A k).indicator (fun (x : Ω) => 1) ω

A count of the elements with a property implying an event is at most the number of events that occur.

def Complexity.Frontier.Gaussian.edgeScoreEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (p : ℝ → Prop) (e : Sym2 W) : Set (W → ℝ)

An event about one edge score.

Equations

• Complexity.Frontier.Gaussian.edgeScoreEvent H q R p e = {ω : W → ℝ | p (Complexity.Frontier.Gaussian.edgeScore H q R ω e)}

theorem Complexity.Frontier.Gaussian.measurableSet_edgeScoreEvent {W : Type} [Fintype W] {H : SimpleGraph W} (q : ℝ) (R : ℕ) {p : ℝ → Prop} (hp : MeasurableSet {x : ℝ | p x}) (e : Sym2 W) : MeasurableSet (edgeScoreEvent H q R p e)

theorem Complexity.Frontier.Gaussian.dependsOn_edgeScoreEvent {W : Type} [Fintype W] [DecidableEq W] {H : SimpleGraph W} (q : ℝ) (R : ℕ) (p : ℝ → Prop) (e : Sym2 W) : DependsOn (fun (x : W → ℝ) => x ∈ edgeScoreEvent H q R p e) ↑(edgeSupport H R e)

theorem Complexity.Frontier.Gaussian.sum_edgeVector_sq_of_mem {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) {q : ℝ} (hq0 : 0 ≤ q) {R : ℕ} {ρ₀ : ℝ} (hρ₀ : -1 < ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) {e : Sym2 W} (he : e ∈ H.edgeFinset) : ∑ z : W, edgeVector H q R e z ^ 2 = 1

The edge vectors of a graph with large kernel correlations are unit vectors.

noncomputable def Complexity.Frontier.Gaussian.cubicBound (ρ₀ T ε : ℝ) (M : ℕ) : ℝ

The prefix-cut bound of the median layout, per vertex, with the given parameters.

Equations

• Complexity.Frontier.Gaussian.cubicBound ρ₀ T ε M = max (9 / (2 * T ^ 2) + 3 * ε) (Complexity.Frontier.Gaussian.straddleBound ρ₀ + 9 / 2 * (2 * T / ↑M) / √(2 * Real.pi) + 4 * ε)

theorem Complexity.Frontier.Gaussian.exists_good_sample {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) {q : ℝ} (hq0 : 0 ≤ q) (R : ℕ) {ρ₀ : ℝ} (hρ₀ : 17 / 32 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) {T ε : ℝ} (hT : 0 < T) (hε : 0 < ε) {M : ℕ} (hM : 0 < M) (large : (3 * ↑M + 3) * ↑(overlapBound (R + 1)) / ε ^ 2 < ↑(Fintype.card W)) : ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.crossingFinset {w : W | key w < t}).card ≤ ↑(Fintype.card W) * cubicBound ρ₀ T ε M

A good sample. For a large cubic graph some Gaussian sample yields a median layout all of whose prefixes are crossed by at most h · cubicBound ρ₀ T ε M edges.

Parameters

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

theorem Complexity.Frontier.Gaussian.correlation_limit : 2 * (√2 / 2) / (1 + (√2 / 2) ^ 2) = 2 * √2 / 3

theorem Complexity.Frontier.Gaussian.exists_decay_radius {ρ₀ : ℝ} (hρ₀g : ρ₀ < 2 * √2 / 3) : ∃ (q : ℝ) (R : ℕ), 0 ≤ q ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R

Decay rate and radius. Every correlation target below 2√2/3 is met by the truncated kernel for some decay rate q < 1/√2 and some radius.

theorem Complexity.Frontier.Gaussian.gaussianCoefficient_eq : gaussianCoefficient = straddleBound (2 * √2 / 3)

theorem Complexity.Frontier.Gaussian.gaussianCoefficient_ge : 1 / 20 ≤ gaussianCoefficient

theorem Complexity.Frontier.Gaussian.gaussianCoefficient_pos : 0 < gaussianCoefficient

theorem Complexity.Frontier.Gaussian.one_add_inv_two_mul_gaussianCoefficient : 1 + 1 / (2 * gaussianCoefficient) = 1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))

The circuit coefficient 1 + 1/(2p) of the cubic coefficient p.

theorem Complexity.Frontier.Gaussian.two_mul_gaussianCoefficient_le : 2 * gaussianCoefficient ≤ 9 / 32

The layout coefficient 2p is at most 9/32.

theorem Complexity.Frontier.Gaussian.exists_parameters {ξ : ℝ} (hξ : 0 < ξ) : ∃ (q : ℝ) (R : ℕ) (ρ₀ : ℝ) (T : ℝ) (ε : ℝ) (M : ℕ), 0 ≤ q ∧ 17 / 32 ≤ ρ₀ ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R ∧ 0 < T ∧ 0 < ε ∧ 0 < M ∧ cubicBound ρ₀ T ε M ≤ gaussianCoefficient + ξ

Parameters. For every positive slack some admissible parameters bring the per-vertex cut bound within that slack of gaussianCoefficient.

theorem Complexity.Frontier.Gaussian.cubicLayoutBound_gaussian : CubicLayoutBound gaussianCoefficient

Gaussian layouts of cubic graphs. For every ξ > 0, every sufficiently large simple cubic graph on h vertices has a layout whose prefixes are crossed by at most (gaussianCoefficient + ξ) h edges.