Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Gaussian.Frontier.Internal.Vector

Normalized edge sums of kernel rows #

An edge uv carries the unit vector (x_u + x_v) / ‖x_u + x_v‖, where x are the normalized kernel rows. It is supported on the two endpoint balls, and its inner product with either endpoint row is √((1 + ρ) / 2), where ρ = ⟨x_u, x_v⟩.

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

The squared norm of the sum of two kernel rows.

Equations
Instances For
    source
    theorem Algebraic.Cutwidth.Gaussian.Internal.pairNormSq_comm {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) :
    pairNormSq H q R u v = pairNormSq H q R v u
    source
    theorem Algebraic.Cutwidth.Gaussian.Internal.pairNormSq_eq {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v : W) :
    pairNormSq H q R u v = 2 + 2 * ∑ z : W, unitKernel H q R u z * unitKernel H q R v z
    source
    noncomputable def Algebraic.Cutwidth.Gaussian.Internal.edgeVector {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) :
    Sym2 W → W → ℝ

    The unit vector of an edge: the normalized sum of its endpoint kernel rows.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Algebraic.Cutwidth.Gaussian.Internal.edgeVector_mk {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (u v z : W) :
      edgeVector H q R s(u, v) z = (unitKernel H q R u z + unitKernel H q R v z) / √(pairNormSq H q R u v)
      source
      noncomputable def Algebraic.Cutwidth.Gaussian.Internal.edgeScore {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (ω : W → ℝ) (e : Sym2 W) :
      ℝ

      The Gaussian score of an edge.

      Equations
      Instances For
        source
        theorem Algebraic.Cutwidth.Gaussian.Internal.sum_edgeVector_sq {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {u v : W} (hpos : 0 < pairNormSq H q R u v) :
        ∑ z : W, edgeVector H q R s(u, v) z ^ 2 = 1
        source
        theorem Algebraic.Cutwidth.Gaussian.Internal.sum_edgeVector_mul {W : Type} [Fintype W] (H : SimpleGraph W) {q : ℝ} {R : ℕ} {u v : W} (hpos : 0 < pairNormSq H q R u v) :
        ∑ z : W, edgeVector H q R s(u, v) z * unitKernel H q R v z = √((1 + ∑ z : W, unitKernel H q R u z * unitKernel H q R v z) / 2)

        The inner product of an edge vector with the row of an endpoint.

        source
        theorem Algebraic.Cutwidth.Gaussian.Internal.edgeVector_eq_zero {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableEq W] {q : ℝ} {R : ℕ} {e : Sym2 W} {z : W} (hz : z ∉ edgeSupport H R e) :
        edgeVector H q R e z = 0
        source
        theorem Algebraic.Cutwidth.Gaussian.Internal.edgeScore_congr {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableEq W] {q : ℝ} {R : ℕ} {e : Sym2 W} {S : Finset W} (hS : edgeSupport H R e ⊆ S) {ω ω' : W → ℝ} (h : ∀ i ∈ S, ω i = ω' i) :
        edgeScore H q R ω e = edgeScore H q R ω' e
        source
        theorem Algebraic.Cutwidth.Gaussian.Internal.measurable_edgeScore {W : Type} [Fintype W] (H : SimpleGraph W) (q : ℝ) (R : ℕ) (e : Sym2 W) :
        Measurable fun (ω : W → ℝ) => edgeScore H q R ω e