def BooleanAnalysis.indicator {n : ℕ} (A : Finset (Fin n → Bool)) : (Fin n → Bool) → Bool

theorem BooleanAnalysis.indicator_ne_iff {n : ℕ} (A : Finset (Fin n → Bool)) (x y : Fin n → Bool) : indicator A x ≠ indicator A y ↔ x ∈ A ∧ y ∉ A ∨ x ∉ A ∧ y ∈ A

theorem BooleanAnalysis.flipCoord_eq_flip {n : ℕ} (x : Fin n → Bool) (i : Fin n) : BooleanFourier.flipCoord x i = flip x i

theorem BooleanAnalysis.totalInfluence_indicator {n : ℕ} (A : Finset (Fin n → Bool)) : BooleanFourier.totalInfluence (indicator A) = (∑ i : Fin n, ↑{x : Fin n → Bool | x ∈ A ∧ flip x i ∉ A ∨ x ∉ A ∧ flip x i ∈ A}.card) / 2 ^ n

theorem BooleanAnalysis.card_boundary_eq_sum {n : ℕ} (A : Finset (Fin n → Bool)) : {p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ flip p.1 p.2 ∉ A ∨ p.1 ∉ A ∧ flip p.1 p.2 ∈ A}.card = ∑ i : Fin n, {x : Fin n → Bool | x ∈ A ∧ flip x i ∉ A ∨ x ∉ A ∧ flip x i ∈ A}.card

theorem BooleanAnalysis.edgeBoundaryMeasure_eq_totalInfluence_indicator_div_n {n : ℕ} (hn : n ≠ 0) (A : Finset (Fin n → Bool)) : edgeBoundaryMeasure n A = BooleanFourier.totalInfluence (indicator A) / ↑n