Gaussian vertex layouts in bounded degree

Normalize the truncated radial kernel at each vertex, take its Gaussian score, and sort. Every edge crosses a fixed threshold with probability at most arccos(ρ) / π. Local dependence controls a finite grid of cuts, score windows, and tails simultaneously. The deterministic ordering lemma then controls all prefixes, including ties.

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

A vertex's unit radial-kernel Gaussian score.

Equations

• Complexity.Frontier.Gaussian.vertexScore H q R ω v = Complexity.Frontier.Gaussian.form (Complexity.Frontier.Gaussian.unitKernel H q R v) ω

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

The event that a vertex's score satisfies p.

Equations

• Complexity.Frontier.Gaussian.vertexEvent H q R p v = {ω : W → ℝ | p (Complexity.Frontier.Gaussian.vertexScore H q R ω v)}

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

The event that the threshold t separates the scores of an edge's endpoints.

Equations

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

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

theorem Complexity.Frontier.Gaussian.measurableSet_crossingEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (t : ℝ) (e : Sym2 W) : MeasurableSet (crossingEvent H q R t e)

theorem Complexity.Frontier.Gaussian.vertexScore_congr {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (v : W) {ω ω' : W → ℝ} (h : ∀ z ∈ ball H v R, ω z = ω' z) : vertexScore H q R ω v = vertexScore H q R ω' v

theorem Complexity.Frontier.Gaussian.dependsOn_vertexEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (p : ℝ → Prop) (v : W) : DependsOn (fun (x : W → ℝ) => x ∈ vertexEvent H q R p v) ↑(ball H v R)

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

def Complexity.Frontier.Gaussian.vertexOverlap (d R : ℕ) : ℕ

One overlap bound suffices for both vertex and edge events.

Equations

• Complexity.Frontier.Gaussian.vertexOverlap d R = d ^ (2 * R + 3)

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

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

theorem Complexity.Frontier.Gaussian.measureReal_crossingEvent_le {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (hd : 2 ≤ d) (degree : ∀ (v : W), H.degree v ≤ d) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) {ρ : ℝ} (hρ0 : -1 < ρ) (hρ : ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * (↑(d - 1) * q ^ 2) ^ R) (t : ℝ) {e : Sym2 W} (he : e ∈ H.edgeFinset) : (gaussPi W).real (crossingEvent H q R t e) ≤ Real.arccos ρ / Real.pi

theorem Complexity.Frontier.Gaussian.card_edges_le_degree_mul {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (degree : ∀ (v : W), H.degree v ≤ d) : H.edgeFinset.card ≤ d * Fintype.card W

A bounded-degree graph has at most d |V| edges (the weaker form of handshaking convenient for the concentration constants).

theorem Complexity.Frontier.Gaussian.exists_vertex_sample {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (hd : 2 ≤ d) (degree : ∀ (v : W), H.degree v ≤ d) {q : ℝ} (hq : 0 ≤ q) (R : ℕ) {ρ : ℝ} (hρ0 : -1 < ρ) (hρ : ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * (↑(d - 1) * q ^ 2) ^ R) {T ε : ℝ} (hT : 0 < T) (hε : 0 < ε) {M : ℕ} (hM : 0 < M) (large : (↑M * (↑d + 1) + 2) * ↑(vertexOverlap d R) / ε ^ 2 < ↑(Fintype.card W)) : ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.crossingFinset {v : W | key v < t}).card ≤ Real.arccos ρ / Real.pi * ↑H.edgeFinset.card + ↑(Fintype.card W) * (↑d / T ^ 2 + ↑d * (2 * T / ↑M) / √(2 * Real.pi) + (↑d + 1) * ε)

Simultaneous control of all grid cuts, vertex windows, and tails. The sample determines an actual vertex ordering, with no distinct-score assumption.