def BooleanFourier.restrict {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (b : Bool) : (Fin n → Bool) → Bool

theorem BooleanFourier.card_filter_cons {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (b : Bool) : {x : Fin (n + 1) → Bool | x 0 = b ∧ f x = true}.card = {y : Fin n → Bool | f (Fin.cons b y) = true}.card

theorem BooleanFourier.filter_card_decomp {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) : {x : Fin (n + 1) → Bool | f x = true}.card = {y : Fin n → Bool | f (Fin.cons false y) = true}.card + {y : Fin n → Bool | f (Fin.cons true y) = true}.card

theorem BooleanFourier.vol_restrict_decomp {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) : vol f = (vol (restrict f false) + vol (restrict f true)) / 2

theorem BooleanFourier.filter_card_split_by_first_coord {n : ℕ} (P : (Fin (n + 1) → Bool) → Prop) [DecidablePred P] : (Finset.filter P Finset.univ).card = {y : Fin n → Bool | P (Fin.cons false y)}.card + {y : Fin n → Bool | P (Fin.cons true y)}.card

theorem BooleanFourier.flipCoord_cons_zero {n : ℕ} (b : Bool) (y : Fin n → Bool) : flipCoord (Fin.cons b y) 0 = Fin.cons (!b) y

theorem BooleanFourier.flipCoord_cons_succ {n : ℕ} (b : Bool) (y : Fin n → Bool) (i : Fin n) : flipCoord (Fin.cons b y) i.succ = Fin.cons b (flipCoord y i)

theorem BooleanFourier.influence_succ_eq {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (i : Fin n) : influence f i.succ = (influence (restrict f false) i + influence (restrict f true) i) / 2

theorem BooleanFourier.card_disagree_ge_abs_diff {α : Type u_1} [Fintype α] [DecidableEq α] (f₀ f₁ : α → Bool) : ↑{y : α | f₀ y ≠ f₁ y}.card ≥ |↑{y : α | f₁ y = true}.card - ↑{y : α | f₀ y = true}.card|

theorem BooleanFourier.influence_zero_ge_abs_vol_diff {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) : influence f 0 ≥ |vol (restrict f true) - vol (restrict f false)|

theorem BooleanFourier.totalInfluence_restrict_bound {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) : totalInfluence f ≥ (totalInfluence (restrict f false) + totalInfluence (restrict f true)) / 2 + |vol (restrict f true) - vol (restrict f false)|

theorem BooleanFourier.tensorization_half (α₀ α₁ : ℝ) (hα₀_pos : 0 < α₀) (hα₁_pos : 0 < α₁) (hα₀_le : α₀ ≤ 1) (hα₁_le : α₁ ≤ 1) : (α₀ * (Real.log (1 / α₀) / Real.log 2) + α₁ * (Real.log (1 / α₁) / Real.log 2)) / 2 + |α₁ - α₀| ≥ (α₀ + α₁) / 2 * (Real.log (1 / ((α₀ + α₁) / 2)) / Real.log 2)

theorem BooleanFourier.tensorization_half_boundary_left (α₁ : ℝ) (hα₁_pos : 0 < α₁) (hα₁_le : α₁ ≤ 1) : (0 * (Real.log (1 / 0) / Real.log 2) + α₁ * (Real.log (1 / α₁) / Real.log 2)) / 2 + |α₁ - 0| ≥ (0 + α₁) / 2 * (Real.log (1 / ((0 + α₁) / 2)) / Real.log 2)

theorem BooleanFourier.tensorization_half_boundary_right (α₀ : ℝ) (hα₀_pos : 0 < α₀) (hα₀_le : α₀ ≤ 1) : (α₀ * (Real.log (1 / α₀) / Real.log 2) + 0 * (Real.log (1 / 0) / Real.log 2)) / 2 + |0 - α₀| ≥ (α₀ + 0) / 2 * (Real.log (1 / ((α₀ + 0) / 2)) / Real.log 2)

theorem BooleanFourier.totalInfluence_ge_two_vol_log {n : ℕ} (f : (Fin n → Bool) → Bool) : totalInfluence f ≥ (1 - vol f) * (Real.log (1 / (1 - vol f)) / Real.log 2)