A good sample for the edge-score decomposition

Fix thresholds -T + i δ with δ = 2T / M. For each threshold count the vertices whose edge scores straddle it and the edges scoring in the following window, and count the edges in both tails. Each count is a sum of local events, so it deviates from its mean by ε h with probability O(1 / h). For large cubic graphs some sample keeps all counts near their means, and the edge-score decomposition of that sample has bags of at most h · frontierLayoutBound ρ₀ T ε M vertices.

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.frontierLayoutBound (ρ₀ T ε : ℝ) (M : ℕ) : ℝ

The bag bound of the edge-score decomposition with the given parameters, per vertex.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.frontierLayoutBound ρ₀ T ε M = max (3 / T ^ 2 + 2 * ε) (Algebraic.Cutwidth.Gaussian.Internal.frontierBound ρ₀ + 3 * (2 * T / ↑M) / √(2 * Real.pi) + 3 * ε)

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_eq_sum_indicator' {Ω κ : Type} (F : Finset κ) (A : κ → Set Ω) (ω : Ω) : ↑{k ∈ F | ω ∈ A k}.card = ∑ k ∈ F, (A k).indicator (fun (x : Ω) => 1) ω

theorem Algebraic.Cutwidth.Gaussian.Internal.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)

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.dependsOn_straddleEvent {W : Type} [Fintype W] [DecidableEq 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))

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

An event about one edge score.

Equations

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

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.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

Edge vectors of a graph with large kernel correlations are unit vectors.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_good_frontier_sample {W : Type} [Fintype W] [DecidableEq 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)) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ ↑(Fintype.card W) * frontierLayoutBound ρ₀ T ε M

A good sample. For a large cubic graph some Gaussian sample yields an edge-score path decomposition whose bags have at most h · frontierLayoutBound ρ₀ T ε M vertices.