Locality of the Gaussian scores

The score of a vertex is a Gaussian form in the coordinates of its kernel ball. Hence the event that a threshold separates the endpoints of an edge depends only on the union of the endpoint balls, and each such union meets the unions of boundedly many edges. The same holds for events about a single score.

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.score {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (ω : W → ℝ) (v : W) : ℝ

The Gaussian score of a vertex at a sample point.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.score H q R ω v = Algebraic.Cutwidth.Gaussian.form (Algebraic.Cutwidth.Gaussian.unitKernel H q R v) ω

theorem Algebraic.Cutwidth.Gaussian.Internal.form_congr {ι : Type} [Fintype ι] {α : ι → ℝ} {S : Finset ι} (hα : ∀ i ∉ S, α i = 0) {ω ω' : ι → ℝ} (h : ∀ i ∈ S, ω i = ω' i) : form α ω = form α ω'

theorem Algebraic.Cutwidth.Gaussian.Internal.score_congr {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {v : W} {S : Finset W} (hS : ball H v R ⊆ S) {ω ω' : W → ℝ} (h : ∀ i ∈ S, ω i = ω' i) : score H q R ω v = score H q R ω' v

theorem Algebraic.Cutwidth.Gaussian.Internal.between_comm {t x y : ℝ} : Between t x y ↔ Between t y x

theorem Algebraic.Cutwidth.Gaussian.Internal.measurableSet_between {Ω : Type} [MeasurableSpace Ω] {f g : Ω → ℝ} (hf : Measurable f) (hg : Measurable g) (t : ℝ) : MeasurableSet {ω : Ω | Between t (f ω) (g ω)}

def Algebraic.Cutwidth.Gaussian.Internal.Crosses {W : Type} (t : ℝ) (X : W → ℝ) : Sym2 W → Prop

A threshold separates the scores of the two endpoints of an edge.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.Crosses t X = Sym2.lift ⟨fun (u v : W) => Algebraic.Cutwidth.Gaussian.Between t (X u) (X v), ⋯⟩

@[simp]

theorem Algebraic.Cutwidth.Gaussian.Internal.crosses_mk {W : Type} {t : ℝ} {X : W → ℝ} {u v : W} : Crosses t X s(u, v) ↔ Between t (X u) (X v)

theorem Algebraic.Cutwidth.Gaussian.Internal.mem_cutFinset_filter_lt_iff {W : Type} [Fintype W] (H : SimpleGraph W) (X : W → ℝ) (t : ℝ) (e : Sym2 W) : e ∈ H.cutFinset {v : W | X v < t} ↔ e ∈ H.edgeSet ∧ Crosses t X e

The cut of a threshold set consists of the edges the threshold separates.

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.edgeSupport {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (R : ℕ) : Sym2 W → Finset W

The coordinates on which the crossing event of an edge depends.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.edgeSupport H R = Sym2.lift ⟨fun (u v : W) => Algebraic.Cutwidth.Gaussian.ball H u R ∪ Algebraic.Cutwidth.Gaussian.ball H v R, ⋯⟩

@[simp]

theorem Algebraic.Cutwidth.Gaussian.Internal.edgeSupport_mk {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (R : ℕ) (u v : W) : edgeSupport H R s(u, v) = ball H u R ∪ ball H v R

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

The crossing event of an edge.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.crossEvent H q R t e = {ω : W → ℝ | Algebraic.Cutwidth.Gaussian.Internal.Crosses t (Algebraic.Cutwidth.Gaussian.Internal.score H q R ω) e}

theorem Algebraic.Cutwidth.Gaussian.Internal.measurableSet_crossEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (t : ℝ) (e : Sym2 W) : MeasurableSet (crossEvent H q R t e)

theorem Algebraic.Cutwidth.Gaussian.Internal.dependsOn_crossEvent {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (t : ℝ) (e : Sym2 W) : DependsOn (fun (x : W → ℝ) => x ∈ crossEvent H q R t e) ↑(edgeSupport H R e)

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

An event about one score.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.scoreEvent H q R p v = {ω : W → ℝ | p (Algebraic.Cutwidth.Gaussian.Internal.score H q R ω v)}

theorem Algebraic.Cutwidth.Gaussian.Internal.dependsOn_scoreEvent {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (p : ℝ → Prop) (v : W) : DependsOn (fun (x : W → ℝ) => x ∈ scoreEvent H q R p v) ↑(ball H v R)

def Algebraic.Cutwidth.Gaussian.Internal.overlapBound (R : ℕ) : ℕ

The overlap constant for supports of radius R.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.overlapBound R = 9 * 2 ^ (2 * R + 2)

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_not_disjoint_edgeSupport_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (R : ℕ) {e : Sym2 W} (he : e ∈ H.edgeFinset) : {l ∈ H.edgeFinset | ¬Disjoint (edgeSupport H R e) (edgeSupport H R l)}.card ≤ overlapBound R

The crossing-event supports of boundedly many edges meet that of a given edge.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_not_disjoint_ball_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (R : ℕ) (v : W) : {w : W | ¬Disjoint (ball H v R) (ball H w R)}.card ≤ overlapBound R

The score-event supports of boundedly many vertices meet that of a given vertex.