Second-moment concentration for counts of locally dependent events

Let Y count the events A k, k ∈ F, of a probability space, and let G be a dependency relation: events A k and A l with ¬ G k l are independent. Then:

• the indicators of A k and A l have covariance zero when ¬ G k l, and at most one always, so Var Y ≤ |F| D when each k ∈ F is related to at most D indices of F (ProbabilityTheory.variance_sum_indicator_le);
• by Chebyshev's inequality, Y deviates from its mean ∑ k, P(A k) by at least c > 0 with probability at most |F| D / c ^ 2 (ProbabilityTheory.measureReal_le_abs_sum_indicator_sub_le).

The motivating dependency relation comes from product spaces. Under a product of probability measures, functions of disjoint sets of coordinates are independent (ProbabilityTheory.indepFun_pi_of_dependsOn), so events determined by the coordinates in sets S k (in the sense of DependsOn) are independent whenever their sets are disjoint (ProbabilityTheory.indepSet_pi_of_dependsOn). Counts of such local events concentrate when each S k meets few of the others (ProbabilityTheory.measureReal_pi_le_abs_sum_indicator_sub_le).

Main results

• ProbabilityTheory.variance_sum_indicator_le: the variance of a count of events with a dependency relation.
• ProbabilityTheory.measureReal_le_abs_sum_indicator_sub_le: the corresponding deviation bound.
• ProbabilityTheory.indepFun_pi_of_dependsOn, ProbabilityTheory.indepSet_pi_of_dependsOn: functions and events of disjoint sets of coordinates are independent under a product measure.
• ProbabilityTheory.measureReal_pi_le_abs_sum_indicator_sub_le: the deviation bound for local events in a product space.

theorem ProbabilityTheory.variance_sum_indicator_le {Ω : Type u_1} {κ : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (F : Finset κ) {A : κ → Set Ω} (hA : ∀ k ∈ F, MeasurableSet (A k)) (G : κ → κ → Prop) [DecidableRel G] (hG : ∀ k ∈ F, ∀ l ∈ F, ¬G k l → IndepSet (A k) (A l) P) {D : ℕ} (hD : ∀ k ∈ F, {l ∈ F | G k l}.card ≤ D) : variance (fun (ω : Ω) => ∑ k ∈ F, (A k).indicator 1 ω) P ≤ ↑F.card * ↑D

The variance of a count of events. If events A k and A l with ¬ G k l are independent, and each k ∈ F is related by G to at most D indices of F, then the number of events A k, k ∈ F, that occur has variance at most |F| D.

theorem ProbabilityTheory.measureReal_le_abs_sum_indicator_sub_le {Ω : Type u_1} {κ : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (F : Finset κ) {A : κ → Set Ω} (hA : ∀ k ∈ F, MeasurableSet (A k)) (G : κ → κ → Prop) [DecidableRel G] (hG : ∀ k ∈ F, ∀ l ∈ F, ¬G k l → IndepSet (A k) (A l) P) {D : ℕ} (hD : ∀ k ∈ F, {l ∈ F | G k l}.card ≤ D) {c : ℝ} (hc : 0 < c) : P.real {ω : Ω | c ≤ |∑ k ∈ F, (A k).indicator 1 ω - ∑ k ∈ F, P.real (A k)|} ≤ ↑F.card * ↑D / c ^ 2

Second-moment concentration. If events A k and A l with ¬ G k l are independent, and each k ∈ F is related by G to at most D indices of F, then the number of events A k, k ∈ F, that occur deviates from its mean by at least c > 0 with probability at most |F| D / c ^ 2.

theorem ProbabilityTheory.indepFun_pi_of_dependsOn {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {β : Type u_3} {γ : Type u_4} [MeasurableSpace β] [MeasurableSpace γ] {f : ((i : ι) → Ω i) → β} {g : ((i : ι) → Ω i) → γ} (hf : Measurable f) (hg : Measurable g) {S T : Set ι} (hfS : DependsOn f S) (hgT : DependsOn g T) (hST : Disjoint S T) : IndepFun f g (MeasureTheory.Measure.pi μ)

Functions of disjoint sets of coordinates are independent under a product of probability measures.

theorem ProbabilityTheory.indepSet_pi_of_dependsOn {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {A B : Set ((i : ι) → Ω i)} (hA : MeasurableSet A) (hB : MeasurableSet B) {S T : Set ι} (hAS : DependsOn (fun (x : (i : ι) → Ω i) => x ∈ A) S) (hBT : DependsOn (fun (x : (i : ι) → Ω i) => x ∈ B) T) (hST : Disjoint S T) : IndepSet A B (MeasureTheory.Measure.pi μ)

Events of disjoint sets of coordinates are independent under a product of probability measures.

theorem ProbabilityTheory.measureReal_pi_le_abs_sum_indicator_sub_le {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {κ : Type u_3} (F : Finset κ) {A : κ → Set ((i : ι) → Ω i)} (hA : ∀ k ∈ F, MeasurableSet (A k)) (S : κ → Set ι) (hAS : ∀ k ∈ F, DependsOn (fun (x : (i : ι) → Ω i) => x ∈ A k) (S k)) (G : κ → κ → Prop) [DecidableRel G] (hG : ∀ k ∈ F, ∀ l ∈ F, ¬G k l → Disjoint (S k) (S l)) {D : ℕ} (hD : ∀ k ∈ F, {l ∈ F | G k l}.card ≤ D) {c : ℝ} (hc : 0 < c) : (MeasureTheory.Measure.pi μ).real {ω : (i : ι) → Ω i | c ≤ |∑ k ∈ F, (A k).indicator 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, let each event A k depend only on the coordinates in S k, where S k and S l are disjoint unless G k l, and let each k ∈ F be related by G to at most D indices of F. Then the number of events A k, k ∈ F, that occur deviates from its mean by at least c > 0 with probability at most |F| D / c ^ 2.