Second moments of local event counts

Under a product of probability measures, two events that depend on disjoint finite sets of coordinates have independent indicators, so their covariance vanishes; any two unit indicators have covariance at most one. Summing over pairs bounds the variance of the event count, and Chebyshev's inequality bounds its deviation.

theorem Algebraic.Cutwidth.Gaussian.Internal.memLp_indicator_one {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.MemLp (s.indicator fun (x : α) => 1) 2 ν

The unit indicator of a measurable set is square integrable under a finite measure.

theorem Algebraic.Cutwidth.Gaussian.Internal.covariance_indicator_le_one {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : ProbabilityTheory.covariance (s.indicator fun (x : α) => 1) (t.indicator fun (x : α) => 1) ν ≤ 1

Two unit indicators have covariance at most one under a probability measure.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_indicator_eq_comp {ι : Type u_1} [DecidableEq ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {S : Finset ι} {A : Set ((i : ι) → Ω i)} (hA : MeasurableSet A) (hdep : ∀ (ω ω' : (i : ι) → Ω i), (∀ i ∈ S, ω i = ω' i) → (ω ∈ A ↔ ω' ∈ A)) (ω₀ : (i : ι) → Ω i) : ∃ (g : ((i : ↥S) → Ω ↑i) → ℝ), Measurable g ∧ (A.indicator fun (x : (i : ι) → Ω i) => 1) = g ∘ fun (ω : (i : ι) → Ω i) (i : ↥S) => ω ↑i

The indicator of a measurable set depending only on the coordinates in S is a measurable function of those coordinates.

theorem Algebraic.Cutwidth.Gaussian.Internal.indepFun_indicator_of_disjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {S T : Finset ι} {A B : Set ((i : ι) → Ω i)} (hA : MeasurableSet A) (hB : MeasurableSet B) (hdepA : ∀ (ω ω' : (i : ι) → Ω i), (∀ i ∈ S, ω i = ω' i) → (ω ∈ A ↔ ω' ∈ A)) (hdepB : ∀ (ω ω' : (i : ι) → Ω i), (∀ i ∈ T, ω i = ω' i) → (ω ∈ B ↔ ω' ∈ B)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (A.indicator fun (x : (i : ι) → Ω i) => 1) (B.indicator fun (x : (i : ι) → Ω i) => 1) (MeasureTheory.Measure.pi μ)

Events depending on disjoint coordinate sets have independent indicators under a product of probability measures.

theorem Algebraic.Cutwidth.Gaussian.Internal.variance_sum_indicator_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {κ : Type u_3} (F : Finset κ) (A : κ → Set ((i : ι) → Ω i)) (S : κ → Finset ι) (measurable : ∀ k ∈ F, MeasurableSet (A k)) (depends : ∀ k ∈ F, ∀ (ω ω' : (i : ι) → Ω i), (∀ i ∈ S k, ω i = ω' i) → (ω ∈ A k ↔ ω' ∈ A 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

The variance of a count of local events is at most the number of events times a bound on how many of their coordinate sets each coordinate set meets.

theorem Algebraic.Cutwidth.Gaussian.Internal.pi_deviation_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {κ : Type u_3} (F : Finset κ) (A : κ → Set ((i : ι) → Ω i)) (S : κ → Finset ι) (measurable : ∀ k ∈ F, MeasurableSet (A k)) (depends : ∀ k ∈ F, ∀ (ω ω' : (i : ι) → Ω i), (∀ i ∈ S k, ω i = ω' i) → (ω ∈ A k ↔ ω' ∈ A 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

Chebyshev for local event counts. The count deviates from its mean by at least c with probability at most |F| D / c².