Gaussian forms and threshold crossings

The sample space for the Gaussian vertex layout is ι → ℝ with independent standard Gaussian coordinates. A coefficient vector α gives the score form α ω = ∑ i, α i * ω i, and Between t x y says that the threshold t separates the two scores x and y, with the lower one strictly below t.

@[reducible, inline]

noncomputable abbrev Algebraic.Cutwidth.Gaussian.gaussPi (ι : Type) [Fintype ι] : MeasureTheory.Measure (ι → ℝ)

The standard Gaussian product measure on ι → ℝ.

Equations

• Algebraic.Cutwidth.Gaussian.gaussPi ι = MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1

instance Algebraic.Cutwidth.Gaussian.instIsProbabilityMeasureForallRealGaussPi (ι : Type) [Fintype ι] : MeasureTheory.IsProbabilityMeasure (gaussPi ι)

noncomputable def Algebraic.Cutwidth.Gaussian.form {ι : Type} [Fintype ι] (α ω : ι → ℝ) : ℝ

The linear form ω ↦ ∑ i, α i * ω i.

Equations

• Algebraic.Cutwidth.Gaussian.form α ω = ∑ i : ι, α i * ω i

def Algebraic.Cutwidth.Gaussian.Between (t x y : ℝ) : Prop

t lies weakly above one value and strictly above the other.

Equations

• Algebraic.Cutwidth.Gaussian.Between t x y = (x < t ∧ t ≤ y ∨ y < t ∧ t ≤ x)