One sample controls every frontier of the median layout

Let G be a loopless multigraph on h vertices in which every vertex has three edges, so that it has 3h/2 edges. Score its edges by a Gaussian sample and lay out its vertices by the medians of their scores (Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_edgeScore), with the grid -T, -T + δ, ..., T of M windows of width δ = 2T / M. Four families of counts control the frontiers: the vertices straddling each grid threshold, the edges scoring in each window, and the edges scoring in each tail.

Each count is a sum of indicators of local events, which concentrates by the second-moment bound (Cslib.Circuits.Frontier.Gaussian.measureReal_deviation_le): it deviates from its mean by ε h with probability O(1 / (ε ^ 2 h)). So for large h a union bound over the 2M + 2 counts leaves a sample at which all of them are within ε h of their means (exists_concentrated_sample). The means are at most μ h straddling vertices at each threshold, (3h/2) δ / √(2π) edges in each window and (3h/2) / T ^ 2 edges in each tail, so the width is at most h · cubicBoundOfMean μ T ε M (Cslib.Circuits.Frontier.Gaussian.exists_good_sample_of_mean), and with the straddling bound, h · cubicBound ρ₀ T ε M (Cslib.Circuits.Frontier.Gaussian.exists_good_sample).

Main definitions

• Cslib.Circuits.Frontier.Gaussian.edgeScoreEvent: an event about the score of one edge.
• Cslib.Circuits.Frontier.Gaussian.cubicBound, Cslib.Circuits.Frontier.Gaussian.cubicBoundOfMean: the width per vertex of the median layout of a good sample.

Main results

• Cslib.Circuits.Frontier.Gaussian.exists_good_sample_of_mean, Cslib.Circuits.Frontier.Gaussian.exists_good_sample: a good sample.

noncomputable def Cslib.Circuits.Frontier.Gaussian.cubicBoundOfMean (μ T ε : ℝ) (M : ℕ) : ℝ

The width per vertex of the median layout of a good sample, when the expected number of vertices straddling any threshold is at most μ per vertex: the tails beyond T, the windows of width 2T / M, and deviations ε per vertex.

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

The width per vertex of the median layout of a good sample, when adjacent kernel rows have inner product at least ρ₀.

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

The event that the score of e satisfies p.

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

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

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

theorem Cslib.Circuits.Frontier.Gaussian.exists_good_sample_of_mean {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} [Finite E] (hloop : G.Loopless) (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hq : 0 ≤ q) (R : ℕ) {ρ₀ : ℝ} (hρ₀ : -1 < ρ₀) (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) * ↑(vertexOverlap 3 R) / ε ^ 2 < ↑(Nat.card V)) {μ : ℝ} (hmean : ∀ (t : ℝ), ∑ v : V, (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (straddleEvent G q R t v) ≤ ↑(Nat.card V) * μ) : ∃ (σ : Layout V), ↑(G.width σ) ≤ ↑(Nat.card V) * cubicBoundOfMean μ T ε M

A good sample, from the mean of the straddling counts. Let G be a loopless multigraph whose vertices have three edges, let adjacent kernel rows have inner product above -1, and let every threshold be straddled by at most μ |V| vertices in expectation. If G has more than (3 M + 3) vertexOverlap 3 R / ε ^ 2 vertices, some Gaussian sample gives a median layout of width at most |V| · cubicBoundOfMean μ T ε M.

theorem Cslib.Circuits.Frontier.Gaussian.exists_good_sample {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {q : ℝ} [Finite V] [Finite E] (hloop : G.Loopless) (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hq : 0 ≤ q) (R : ℕ) {ρ₀ : ℝ} (hρ₀ : 0 ≤ ρ₀) (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) * ↑(vertexOverlap 3 R) / ε ^ 2 < ↑(Nat.card V)) : ∃ (σ : Layout V), ↑(G.width σ) ≤ ↑(Nat.card V) * cubicBound ρ₀ T ε M

A good sample. Let G be a loopless multigraph whose vertices have three edges, and let adjacent kernel rows have inner product at least ρ₀ ≥ 0. If G has more than (3 M + 3) vertexOverlap 3 R / ε ^ 2 vertices, some Gaussian sample gives a median layout of width at most |V| · cubicBound ρ₀ T ε M.