A good Gaussian sample

Fix thresholds -T + i δ with δ = 2T / M. For each threshold count the separated edges and the scores in the following window, and count both tails. Each count deviates from its mean by at least ε h with probability O(1 / h) by the second-moment bound, so for large cubic graphs some sample keeps all 2M + 2 counts within ε h of their means. The grid bound then controls every prefix of that sample's score order.

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

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

Equations

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

theorem Algebraic.Cutwidth.Gaussian.Internal.measurableSet_scoreEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) {p : ℝ → Prop} (hp : MeasurableSet {x : ℝ | p x}) (v : W) : MeasurableSet (scoreEvent H q R p v)

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.deviation {W : Type} [Fintype W] {κ : Type} (F : Finset κ) (A : κ → Set (W → ℝ)) (c : ℝ) : Set (W → ℝ)

The deviation event of a count of local events.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.deviation F A c = {ω : W → ℝ | c ≤ |∑ k ∈ F, (A k).indicator (fun (x : W → ℝ) => 1) ω - ∑ k ∈ F, (Algebraic.Cutwidth.Gaussian.gaussPi W).real (A k)|}

theorem Algebraic.Cutwidth.Gaussian.Internal.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 Algebraic.Cutwidth.Gaussian.Internal.exists_good_sample {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) {q : ℝ} (hq0 : 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 + 2) * ↑(overlapBound R) / ε ^ 2 < ↑(Fintype.card W)) : ∃ (ω : W → ℝ), ∀ (t : ℕ), ↑(H.cutFinset {w : W | scoreKey (score H q R ω) w < t}).card ≤ ↑(Fintype.card W) * layoutBound ρ₀ T ε M

A good sample. For a large cubic graph some Gaussian sample orders the vertices so that every prefix cut is at most h · layoutBound ρ₀ T ε M.