Rectangle bias and prediction agreement

theorem Complexity.Frontier.sumOn_congr {α : Type u_1} [Finite α] {w w' : α → ℝ} {S : Set α} (h : ∀ x ∈ S, w x = w' x) : sumOn w S = sumOn w' S

@[simp]

theorem Complexity.Frontier.sumOn_const {α : Type u_1} [Finite α] (a : ℝ) (S : Set α) : sumOn (fun (x : α) => a) S = a * ↑S.ncard

def Complexity.Frontier.boolSign (b : Bool) : ℝ

A Boolean value as a sign, positive at true.

Equations

• Complexity.Frontier.boolSign b = if b = true then 1 else -1

@[simp]

theorem Complexity.Frontier.abs_boolSign (b : Bool) : |boolSign b| = 1

noncomputable def Complexity.Frontier.agreement {α : Type u_1} (f g : α → Bool) : ℝ

Uniform prediction agreement, normalized by the full input domain.

Equations

• Complexity.Frontier.agreement f g = ↑{x : α | f x = g x}.ncard / ↑(Nat.card α)

def Complexity.Frontier.RectangleBias {ι : Type u_2} {U : Type u_3} [Finite ι] [Finite U] (f : (ι → U) → Bool) (K : ℕ) (β : ℝ) : Prop

Bias at most β on every coordinate rectangle with both sides of size at least K.

Equations

• Complexity.Frontier.RectangleBias f K β = Complexity.Frontier.RectangleBudget (fun (x : ι → U) => Complexity.Frontier.boolSign (f x)) (fun (x : ι → U) => β) K K

theorem Complexity.Frontier.sign_sum_eq {α : Type u_1} [Finite α] (f g : α → Bool) : sumOn (fun (x : α) => boolSign (f x) * boolSign (g x)) Set.univ = 2 * ↑{x : α | f x = g x}.ncard - ↑(Nat.card α)

Signed correlation is twice agreement minus one, before normalization.

theorem Complexity.Frontier.sign_sum_split {α : Type u_1} [Finite α] (f g : α → Bool) : sumOn (fun (x : α) => boolSign (f x) * boolSign (g x)) Set.univ = sumOn (fun (x : α) => boolSign (f x)) {x : α | g x = true} - sumOn (fun (x : α) => boolSign (f x)) {x : α | g x = false}

Splitting by the predicted bit gives the two signed output-class sums.

theorem Complexity.Frontier.agreement_le_of_output_bias {α : Type u_1} [Finite α] [Nonempty α] (f g : α → Bool) {β R : ℝ} (h : ∀ (b : Bool), |sumOn (fun (x : α) => boolSign (f x)) {x : α | g x = b}| ≤ β * ↑{x : α | g x = b}.ncard + R) : agreement f g ≤ (1 + β) / 2 + R / ↑(Nat.card α)

Two output-class bias bounds give the agreement bound with the correct factor of two.

theorem Complexity.Frontier.RectangleBias.abs_sumOn_le_of_dependsOn {ι : Type u_2} {U : Type u_3} [Finite ι] [Finite U] {f : (ι → U) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) {S : Set (ι → U)} {R : Set ι} (hR : DependsOn (fun (x : ι → U) => x ∈ S) R) (hle : K ≤ Nat.card U ^ Rᶜ.ncard) : |sumOn (fun (x : ι → U) => boolSign (f x)) S| ≤ β * ↑S.ncard + ↑(Nat.card U * K ^ 2)

If many inputs are unused, an output class is either a thick rectangle or has only q K² inputs. This is the weighted replacement for the support lemma.

@[simp]

theorem Complexity.Frontier.boolSign_not (b : Bool) : (boolSign !b) = -boolSign b

theorem Complexity.Frontier.RectangleBias.not {ι : Type u_2} {U : Type u_3} [Finite ι] [Finite U] {f : (ι → U) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) : RectangleBias (fun (x : ι → U) => !f x) K β

Complementing the target preserves its rectangle-bias guarantee.

theorem Complexity.Frontier.agreement_not {α : Type u_1} [Finite α] [Nonempty α] (f g : α → Bool) : agreement (fun (x : α) => !f x) g = 1 - agreement f g

Exactly one of a target and its complement agrees with a Boolean prediction.