Common Utilities for LCS Games

This module provides technical lemmas and definitions for signs, indicator functions, and basic properties of the outcome space $\mathbb{F}_2$.

Key Definitions

• observableSign: Returns $1$ if $a=0$ or $-1$ if $a=1$.

Key Lemmas

• sign_mul: The product of signs corresponds to the sum in $\mathbb{F}_2$.
• sign_indicator: Relates the sign-based expression $(1/2)(1 + (-1)^{b+s})$ to the Kronecker delta.

theorem MIPRE.LCS.zmod_two_eq_zero_or_one (a : ZMod 2) : a = 0 ∨ a = 1

Case analysis for ZMod 2.

@[simp]

theorem MIPRE.LCS.zmod_two_val_one : ZMod.val 1 = 1

theorem MIPRE.LCS.sum_univ_zmod_two {M : Type u_1} [AddCommMonoid M] (f : ZMod 2 → M) : ∑ x : ZMod 2, f x = f 0 + f 1

The ZMod 2 counterpart of Fin.sum_univ_two.

theorem MIPRE.LCS.sign_mul (a b : ZMod 2) : (-1) ^ a.val * (-1) ^ b.val = (-1) ^ (a + b).val

theorem MIPRE.LCS.sign_indicator (b s : ZMod 2) : 1 / 2 + 1 / 2 * (-1) ^ b.val * (-1) ^ s.val = if s = b then 1 else 0

Arithmetic helper: the sign factor $(1/2)(1 + (-1)^b * (-1)^s)$ equals the indicator s = b.

def MIPRE.LCS.observableSign (a : ZMod 2) : ℂ

The sign (-1)^a of an 𝔽₂-value: 1 for a = 0 and -1 for a = 1.

Equations

• MIPRE.LCS.observableSign a = if a = 0 then 1 else -1

theorem MIPRE.LCS.sign_sq (x : ZMod 2) : (-1) ^ x.val * (-1) ^ x.val = 1

theorem MIPRE.LCS.prod_sign_eq_sum_sign_aux {G : Layout} {i : Fin G.r} (x : G.Assignment i) (s : Finset ↥(G.V i)) : ∏ j ∈ s, (-1) ^ (x j).val = (-1) ^ (∑ j ∈ s, x j).val

theorem MIPRE.LCS.prod_sign_eq_sum_sign {G : Layout} (i : Fin G.r) (x : G.Assignment i) : ∏ j ∈ (G.V i).attach, (-1) ^ (x j).val = (-1) ^ (∑ j : ↥(G.V i), x j).val

theorem MIPRE.LCS.finset_filter_eq_inter_univ_filter {α : Type u_1} [Fintype α] [DecidableEq α] (S : Finset α) (p : α → Prop) [DecidablePred p] : Finset.filter p S = S ∩ Finset.filter p Finset.univ