The straddling probability of one vertex

Let G be a loopless multigraph in which every vertex has three edges, and let the unit kernel rows of adjacent vertices have inner product at least ρ₀ ≥ 0. The three edge vectors at a vertex v then have inner product at least κ = √((1 + ρ₀)/2) ≥ √2/2 with the row of v: they lie in a spherical cap.

• If v straddles a threshold t, then t lies between the scores of at least four of the six ordered pairs of distinct edges at v.
• By Sheppard's bound [She99], a pair of edges at angle θ is separated by t with probability at most θ / π.
• In the cap the inner products of the pairs lie in [0, 1], where arccos is concave, so if they sum to at least 6 a the angles sum to at most 6 arccos a (Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le_of_average). They sum to at least 9 κ ^ 2 - 3 (InnerProductGeometry.le_sum_offDiag_inner).

Hence v straddles t with probability at most (1/4) (6 / π) arccos ((3 κ ^ 2 - 1)/2) = (3 / (2π)) arccos ((1 + 3 ρ₀)/4) (Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le).

Main definitions

• Cslib.Circuits.Frontier.Gaussian.straddleBound: the bound (3 / (2π)) arccos ((1 + 3 ρ₀)/4).
• Cslib.Circuits.Frontier.Gaussian.straddleEvent: the event that a vertex straddles a threshold.

Main results

• Cslib.Circuits.Frontier.Gaussian.dependsOn_straddleEvent: locality of straddling.
• Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le_of_average, Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le: the straddling probability.

References

• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation

noncomputable def Cslib.Circuits.Frontier.Gaussian.straddleBound (ρ₀ : ℝ) : ℝ

The bound (3 / (2π)) arccos ((1 + 3 ρ₀)/4) on the probability that a vertex straddles a threshold, when adjacent kernel rows have inner product at least ρ₀.

def Cslib.Circuits.Frontier.Gaussian.straddleEvent {V : Type u_1} {E : Type u_2} [Fintype V] (G : Multigraph V E) (q : ℝ) (R : ℕ) (t : ℝ) (v : V) : Set (V → ℝ)

The event that the edge scores at v straddle the threshold t.

theorem Cslib.Circuits.Frontier.Gaussian.measurableSet_straddleEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} [Finite E] (q : ℝ) (R : ℕ) (t : ℝ) (v : V) : MeasurableSet (straddleEvent G q R t v)

Whether a vertex straddles a threshold is a measurable event.

theorem Cslib.Circuits.Frontier.Gaussian.dependsOn_straddleEvent {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} (q : ℝ) (R : ℕ) (t : ℝ) (v : V) : DependsOn (fun (x : V → ℝ) => x ∈ straddleEvent G q R t v) (closedBall G.toSimpleGraph v (R + 1))

Locality. Whether v straddles a threshold depends only on the coordinates of the sample in the closed ball of radius R + 1 around v.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le_of_average {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {ρ₀ : ℝ} [Finite E] (hloop : G.Loopless) (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hq : 0 ≤ q) (hρ₀ : 0 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) (t : ℝ) {v : V} {s : Finset E} (hs : ↑s = G.incidenceSet v) {a : ℝ} (haverage : 6 * a ≤ ∑ p ∈ s.offDiag, inner ℝ (edgeVector G q R p.1) (edgeVector G q R p.2)) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (straddleEvent G q R t v) ≤ 3 / (2 * Real.pi) * Real.arccos a

The straddling probability, from the average inner product. In a loopless multigraph in which every vertex has three edges, let adjacent kernel rows have inner product at least ρ₀ ≥ 0. If the inner products of the edge vectors at v, over the ordered pairs of distinct edges, sum to at least 6 a, then v straddles any fixed threshold with probability at most (3 / (2π)) arccos a.

theorem Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le {V : Type u_1} {E : Type u_2} [Fintype V] {G : Multigraph V E} {q : ℝ} {R : ℕ} {ρ₀ : ℝ} [Finite E] (hloop : G.Loopless) (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hq : 0 ≤ q) (hρ₀ : 0 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) (t : ℝ) (v : V) : (MeasureTheory.Measure.pi fun (x : V) => ProbabilityTheory.gaussianReal 0 1).real (straddleEvent G q R t v) ≤ straddleBound ρ₀

The straddling probability. In a loopless multigraph in which every vertex has three edges, if adjacent kernel rows have inner product at least ρ₀ ≥ 0, then each vertex straddles each threshold with probability at most straddleBound ρ₀.