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.

• Two events whose coordinate sets are disjoint are functions of disjoint blocks of independent coordinates, so their indicators are independent and have covariance zero.
• Any two indicators have covariance at most one.

Summing the covariances over pairs gives 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 ^ 2. Locality is expressed by Mathlib's DependsOn, and the coordinate spaces are arbitrary.

Main results

• Frontier.Gaussian.pi_variance_sum_indicator_le: Var Y ≤ |F| D.
• Frontier.Gaussian.pi_deviation_le: P(|Y - E Y| ≥ c) ≤ |F| D / c ^ 2.

theorem Complexity.Frontier.Gaussian.pi_variance_sum_indicator_le {ι : Type u_3} {κ : Type u_4} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_5} [(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 Complexity.Frontier.Gaussian.pi_deviation_le {ι : Type u_3} {κ : Type u_4} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_5} [(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 ^ 2, when each event depends on a finite set of coordinates and each coordinate set meets at most D of them.