Expected straddling vertices of the edge-score order

A threshold separates two Gaussian edge scores with probability at most arccos ρ' / π (Sheppard's bound), where ρ' is the correlation of the edge vectors. The three edge vectors at a vertex are within correlation √((1 + ρ₀)/2) of the vertex row, so the star inequality bounds their summed angles. A straddling vertex has at least four separated ordered pairs, so it straddles a threshold with probability at most (3/(2π)) arccos ((1 + 3ρ₀)/4). The threshold-decay crossing bound multiplies this by exp (-t²/2) at the threshold t.

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

The per-vertex straddling bound for edge correlations at least ρ₀.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.frontierBound ρ₀ = 3 / (2 * Real.pi) * Real.arccos ((1 + 3 * ρ₀) / 4)

def Algebraic.Cutwidth.Gaussian.Internal.straddleEvent {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℝ) (R : ℕ) (t : ℝ) (v : W) : Set (W → ℝ)

The event that the edge scores at v straddle t.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.straddleEvent H q R t v = {ω : W → ℝ | Algebraic.Cutwidth.Gaussian.EdgeStraddles H (Algebraic.Cutwidth.Gaussian.Internal.edgeScore H q R ω) t v}

theorem Algebraic.Cutwidth.Gaussian.Internal.edgeVector_star {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) (v : W) {e : Sym2 W} (he : e ∈ H.incidenceFinset v) : ∑ z : W, edgeVector H q R e z ^ 2 = 1 ∧ √((1 + ρ₀) / 2) ≤ ∑ z : W, edgeVector H q R e z * unitKernel H q R v z

The edges at a vertex of a graph whose edges have kernel correlation at least ρ₀.

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_straddleEvent_le_of_crossing {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 : ℝ) (v : W) {m : ℝ} (hm : 0 ≤ m) (crossing : ∀ {α β : W → ℝ}, ∑ z : W, α z ^ 2 = 1 → ∑ z : W, β z ^ 2 = 1 → -1 < ∑ z : W, α z * β z → (gaussPi W).real {ω : W → ℝ | Between t (form α ω) (form β ω)} ≤ m * (Real.arccos (∑ z : W, α z * β z) / Real.pi)) : (gaussPi W).real (straddleEvent H q R t v) ≤ m * frontierBound ρ₀

Straddling probability from a crossing bound. If at the threshold t every pair of unit forms with correlation ρ' > -1 is separated with probability at most m · arccos ρ' / π, then a vertex straddles t with probability at most m · frontierBound ρ₀.

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_straddleEvent_le {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 : ℝ) (v : W) : (gaussPi W).real (straddleEvent H q R t v) ≤ frontierBound ρ₀

Straddling probability.

theorem Algebraic.Cutwidth.Gaussian.Internal.measureReal_straddleEvent_le_exp {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 : ℝ) (v : W) : (gaussPi W).real (straddleEvent H q R t v) ≤ Real.exp (-t ^ 2 / 2) * frontierBound ρ₀

Straddling probability away from the median. A vertex straddles the threshold t with probability at most exp (-t²/2) · frontierBound ρ₀.