Expected counts for the Gaussian layout

Adjacent kernel rows have correlation at least ρ₀, so a threshold separates the scores of an edge's endpoints with probability at most crossBound ρ₀. A unit score lies in a window of width δ with probability at most δ / √(2π), and beyond ±T with probability at most 1 / T². Counts of events are written as sums of indicators.

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.crossBound (ρ₀ : ℝ) : ℝ

The crossing-probability bound for edges whose kernel correlation is at least ρ₀.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.crossBound ρ₀ = 2 / Real.pi * (√(1 - ρ₀) / √(1 + ρ₀))

theorem Algebraic.Cutwidth.Gaussian.Internal.sum_add_sq {ι : Type} [Fintype ι] (α β : ι → ℝ) : ∑ i : ι, (α i + β i) ^ 2 = ∑ i : ι, α i ^ 2 + 2 * ∑ i : ι, α i * β i + ∑ i : ι, β i ^ 2

theorem Algebraic.Cutwidth.Gaussian.Internal.sum_sub_sq {ι : Type} [Fintype ι] (α β : ι → ℝ) : ∑ i : ι, (β i - α i) ^ 2 = ∑ i : ι, α i ^ 2 - 2 * ∑ i : ι, α i * β i + ∑ i : ι, β i ^ 2

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_between_le_crossBound {ι : Type} [Fintype ι] {α β : ι → ℝ} (hα : ∑ i : ι, α i ^ 2 = 1) (hβ : ∑ i : ι, β i ^ 2 = 1) {ρ₀ : ℝ} (hρ₀ : -1 < ρ₀) (hρ : ρ₀ ≤ ∑ i : ι, α i * β i) (t : ℝ) : (gaussPi ι).real {ω : ι → ℝ | Between t (form α ω) (form β ω)} ≤ crossBound ρ₀

Two unit coefficient vectors with correlation at least ρ₀ > -1 cross a threshold with probability at most crossBound ρ₀.

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_crossEvent_le {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) (t : ℝ) {e : Sym2 W} (he : e ∈ H.edgeFinset) : (gaussPi W).real (crossEvent H q R t e) ≤ crossBound ρ₀

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

The event that a score lies in the window [s, s + δ).

Equations

• Algebraic.Cutwidth.Gaussian.Internal.windowEvent H q R s δ v = Algebraic.Cutwidth.Gaussian.Internal.scoreEvent H q R (fun (x : ℝ) => s ≤ x ∧ x < s + δ) v

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_windowEvent_le {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (s : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) (v : W) : (gaussPi W).real (windowEvent H q R s δ v) ≤ δ / √(2 * Real.pi)

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_lowEvent_le {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) {T : ℝ} (hT : 0 < T) (v : W) : (gaussPi W).real (scoreEvent H q R (fun (x : ℝ) => x < -T) v) ≤ 1 / T ^ 2

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_highEvent_le {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) {T : ℝ} (hT : 0 < T) (v : W) : (gaussPi W).real (scoreEvent H q R (fun (x : ℝ) => T ≤ x) v) ≤ 1 / T ^ 2

theorem Algebraic.Cutwidth.Gaussian.Internal.card_cutFinset_eq_sum_indicator {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (t : ℝ) (ω : W → ℝ) [Fintype ↑H.edgeSet] : ↑(H.cutFinset {v : W | score H q R ω v < t}).card = ∑ e ∈ H.edgeFinset, (crossEvent H q R t e).indicator (fun (x : W → ℝ) => 1) ω

The cut of a threshold set counts the crossing events of the edges.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_eq_sum_indicator {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (p : ℝ → Prop) [DecidablePred p] (ω : W → ℝ) : ↑{v : W | p (score H q R ω v)}.card = ∑ v : W, (scoreEvent H q R p v).indicator (fun (x : W → ℝ) => 1) ω

A count of score events is the sum of their indicators.