Second-moment concentration for local events

Let Y count the events A k, k ∈ F, under a product of probability measures, where each event depends only on the coordinates in a finite set S k, and each S k meets at most D of the sets S l, l ∈ F. Indicators of events with disjoint coordinate sets are independent, so their covariance vanishes; every other pair has covariance at most one. Hence Var Y ≤ |F| D, and Chebyshev's inequality bounds the probability that Y deviates from its mean ∑ k, P(A k) by at least c by |F| D / c².

Both theorems hold for any product of probability measures on measurable spaces, with locality expressed by Mathlib's DependsOn.

theorem Algebraic.Cutwidth.Gaussian.pi_variance_sum_indicator_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_3} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (F : Finset κ) (A : κ → Set ((i : ι) → Ω i)) (S : κ → Finset ι) (measurable : ∀ k ∈ F, MeasurableSet (A k)) (depends : ∀ k ∈ F, DependsOn (fun (x : (i : ι) → Ω i) => x ∈ A k) ↑(S k)) {D : ℕ} (overlap : ∀ k ∈ F, {l ∈ F | ¬Disjoint (S k) (S l)}.card ≤ D) : ProbabilityTheory.variance (fun (ω : (i : ι) → Ω i) => ∑ k ∈ F, (A k).indicator (fun (x : (i : ι) → Ω i) => 1) ω) (MeasureTheory.Measure.pi μ) ≤ ↑F.card * ↑D

Variance of a count of local events. Under a product of probability measures, if each event depends only on the coordinates in S k and each S k meets at most D of the coordinate sets, the number of events that occur has variance at most |F| D.

theorem Algebraic.Cutwidth.Gaussian.pi_deviation_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_3} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (F : Finset κ) (A : κ → Set ((i : ι) → Ω i)) (S : κ → Finset ι) (measurable : ∀ k ∈ F, MeasurableSet (A k)) (depends : ∀ k ∈ F, DependsOn (fun (x : (i : ι) → Ω i) => x ∈ A k) ↑(S k)) {D : ℕ} (overlap : ∀ k ∈ F, {l ∈ F | ¬Disjoint (S k) (S l)}.card ≤ D) {c : ℝ} (hc : 0 < c) : (MeasureTheory.Measure.pi μ).real {ω : (i : ι) → Ω i | c ≤ |∑ k ∈ F, (A k).indicator (fun (x : (i : ι) → Ω i) => 1) ω - ∑ k ∈ F, (MeasureTheory.Measure.pi μ).real (A k)|} ≤ ↑F.card * ↑D / c ^ 2

Second-moment concentration for local events. Under a product of probability measures on arbitrary measurable spaces, the number of events that occur deviates from its mean by at least c with probability at most |F| D / c², when each event depends on a finite set of coordinates and each coordinate set meets at most D of them.