A good sample for the band-jump decomposition

Fix 0 < c < T. The band-jump decomposition (Gaussian.Band.Order) needs bounds at the thresholds outside the band [-c, c) and, for every block of band edges, on the vertices straddling ±c plus the vertices of the block. Take the blocks to be the band clusters.

• Outside the band, a low grid on [-T, -c] and a high grid on [c, T] with M steps each, and the two tails, are controlled by second-moment deviations as for the edge-score decomposition. Every grid point t has |t| ≥ c, so its straddling probability is at most exp (-c²/2) · frontierBound ρ₀.
• The vertices of a block lie in one band cluster. Either that cluster has at most K vertices, or all of them lie in clusters of more than K vertices. If the expected number of the latter is at most η h, Markov's inequality keeps it below 2 η h with probability at least 1/2.

For large cubic graphs some sample avoids every bad event, and the bags of its band-jump decomposition have at most h · bandLayoutBound ρ₀ c T ε η M + K vertices.

Measurability of the cluster event

def Algebraic.Cutwidth.Gaussian.Internal.maskGraph {W : Type} (H : SimpleGraph W) (β : Sym2 W → Bool) : SimpleGraph W

The graph of the edges of H selected by a Boolean mask.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.maskGraph H β = { Adj := fun (u v : W) => H.Adj u v ∧ β s(u, v) = true, symm := ⋯, loopless := ⋯ }

theorem Algebraic.Cutwidth.Gaussian.Internal.bandGraph_eq_maskGraph {W : Type} (H : SimpleGraph W) (score : Sym2 W → ℝ) (c : ℝ) : bandGraph H score c = maskGraph H fun (e : Sym2 W) => decide (-c ≤ score e ∧ score e < c)

theorem Algebraic.Cutwidth.Gaussian.Internal.measurableSet_bigBandEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (c : ℝ) (K : ℕ) (v : W) : MeasurableSet (bigBandEvent H q R c K v)

The cluster event depends on the sample only through the finitely many band indicators.

theorem Algebraic.Cutwidth.Gaussian.Internal.mem_bigBandEvent {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {c : ℝ} {K : ℕ} {v : W} {ω : W → ℝ} : ω ∈ bigBandEvent H q R c K v ↔ K < {u : W | (bandGraph H (edgeScore H q R ω) c).Reachable v u}.card

Blocks of band edges

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.bandBlock {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (score : Sym2 W → ℝ) (c : ℝ) (e : Sym2 W) : ℕ

The block of an edge: the index of the band cluster of one of its endpoints.

Equations

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

theorem Algebraic.Cutwidth.Gaussian.Internal.connectedComponentMk_out_eq {W : Type} (H : SimpleGraph W) {score : Sym2 W → ℝ} {c : ℝ} {e : Sym2 W} (he : e ∈ H.edgeSet) (hband : -c ≤ score e ∧ score e < c) {v : W} (hv : v ∈ e) : (bandGraph H score c).connectedComponentMk (Quot.out e).1 = (bandGraph H score c).connectedComponentMk v

A band edge of H at v lies in the band cluster of v.

theorem Algebraic.Cutwidth.Gaussian.Internal.bandBlock_eq {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (v : W) (e : Sym2 W) : e ∈ H.incidenceFinset v → ∀ e' ∈ H.incidenceFinset v, -c ≤ score e → score e < c → -c ≤ score e' → score e' < c → bandBlock H score c e = bandBlock H score c e'

Band edges sharing a vertex share a block.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_bandBlock_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (K j : ℕ) : ↑{v : W | ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ bandBlock H score c e = j}.card ≤ ↑K + ↑{v : W | K < {u : W | (bandGraph H score c).Reachable v u}.card}.card

Vertices of a block. The vertices touching the band edges of one block lie in one band cluster, so they number at most K or lie in clusters of more than K vertices.

Markov's inequality for a count of events

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_two_mul_le_sum_indicator_le {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : Finset ι) (A : ι → Set Ω) (hA : ∀ i ∈ F, MeasurableSet (A i)) {m : ℝ} (hm : 0 < m) (hsum : ∑ i ∈ F, μ.real (A i) ≤ m) : μ.real {ω : Ω | 2 * m ≤ ∑ i ∈ F, (A i).indicator (fun (x : Ω) => 1) ω} ≤ 1 / 2

If the expected number of events is at most m > 0, at least 2 m of them occur with probability at most 1/2.

The good sample

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

The bag bound of the band-jump decomposition with the given parameters, per vertex, before the additive cluster size K.

Equations

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

theorem Algebraic.Cutwidth.Gaussian.Internal.frontierBound_nonneg (ρ₀ : ℝ) : 0 ≤ frontierBound ρ₀

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_good_band_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) {c T ε η : ℝ} (hc : 0 < c) (hcT : c < T) (hε : 0 < ε) (hη : 0 < η) {M : ℕ} (hM : 0 < M) {K : ℕ} (hK : ∑ v : W, (gaussPi W).real (bigBandEvent H q R c K v) ≤ η * ↑(Fintype.card W)) (large : (10 * ↑M + 10) * ↑(overlapBound (R + 1)) / ε ^ 2 < ↑(Fintype.card W)) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ ↑(Fintype.card W) * bandLayoutBound ρ₀ c T ε η M + ↑K

A good sample. If the expected number of vertices in band clusters of more than K vertices is at most η h, a large cubic graph has a band-jump path decomposition whose bags have at most h · bandLayoutBound ρ₀ c T ε η M + K vertices.