Correlation through rectangle classes

Suppose the inputs are partitioned into classes, each a rectangle for one fixed cut X, and a predictor g is constant on every class. Lindsey's lemma bounds the signed sum of the quadratic form on each class, and Cauchy–Schwarz over the classes gives

(2 · agreement(f, g) - 1)² · 2^{cutRank Q X} ≤ #classes.

theorem Complexity.Correlation.two_mul_agreement_sub_one {α : Type u_1} [Fintype α] [Nonempty α] (f g : α → Bool) : 2 * Frontier.agreement f g - 1 = (∑ x : α, Frontier.boolSign (f x) * Frontier.boolSign (g x)) / ↑(Fintype.card α)

Twice the agreement minus one is the normalized signed correlation.

theorem Complexity.Correlation.sq_sum_le_of_classes {α : Type u_1} [Fintype α] {M : Type u_2} [Fintype M] [DecidableEq M] (w : α → ℝ) (msg : α → M) (Λ : ℝ) (h : ∀ (x₀ : α), (∑ x : α with msg x = msg x₀, w x) ^ 2 ≤ ↑{x : α | msg x = msg x₀}.card * Λ) : (∑ x : α, w x) ^ 2 ≤ ↑(Fintype.card M) * (↑(Fintype.card α) * Λ)

Cauchy–Schwarz over classes. If the squared sum over every class is at most its size times Λ, the squared total is at most the number of classes times |α| Λ.

theorem Complexity.Correlation.sq_two_mul_agreement_sub_one_mul_le {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Q : Matrix ι ι (ZMod 2)) (g : (ι → Bool) → Bool) {M : Type u_3} [Fintype M] [DecidableEq M] (msg : (ι → Bool) → M) (X : Set ι) (hg : ∀ (x y : ι → Bool), msg x = msg y → g x = g y) (hrect : ∀ (x₀ : ι → Bool), ∃ (A : Set (↑X → Bool)) (B : Set (↑Xᶜ → Bool)), {x : ι → Bool | msg x = msg x₀} = Frontier.rectangle X A B) : (2 * Frontier.agreement (quadForm Q) g - 1) ^ 2 * 2 ^ cutRank Q X ≤ ↑(Fintype.card M)

Correlation through rectangle classes. Let every class of msg be a rectangle for the cut X, and let g be constant on the classes. Then the correlation of g with the quadratic form of Q satisfies (2 · agreement - 1)² · 2^{cutRank Q X} ≤ |M|.