def BooleanFourier.flipBit {n : ℕ} (x : Fin n → Bool) (i : Fin n) : Fin n → Bool

@[simp]

theorem BooleanFourier.flipBit_apply_same {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit x i i = !x i

@[simp]

theorem BooleanFourier.flipBit_apply_ne {n : ℕ} (x : Fin n → Bool) {i k : Fin n} (h : k ≠ i) : flipBit x i k = x k

theorem BooleanFourier.flipBit_flipBit {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit (flipBit x i) i = x

noncomputable def BooleanFourier.pBiasedWeight (n : ℕ) (p : ℝ) (x : Fin n → Bool) : ℝ

noncomputable def BooleanFourier.pBiasedExpectation {n : ℕ} (f : (Fin n → Bool) → Bool) (p : ℝ) : ℝ

noncomputable def BooleanFourier.pBiasedInfluence {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) (p : ℝ) : ℝ

theorem BooleanFourier.hasDerivAt_factor (b : Bool) (p : ℝ) : HasDerivAt (fun (q : ℝ) => if b = true then q else 1 - q) (if b = true then 1 else -1) p

theorem BooleanFourier.hasDerivAt_pBiasedWeight (n : ℕ) (x : Fin n → Bool) (p : ℝ) : HasDerivAt (fun (q : ℝ) => pBiasedWeight n q x) (∑ j : Fin n, (∏ i ∈ Finset.univ.erase j, if x i = true then p else 1 - p) * if x j = true then 1 else -1) p

theorem BooleanFourier.deriv_term_eq_influence {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (j : Fin n) (p : ℝ) (_hp0 : 0 < p) (_hp1 : p < 1) : (∑ x : Fin n → Bool, ((∏ i ∈ Finset.univ.erase j, if x i = true then p else 1 - p) * if x j = true then 1 else -1) * if f x = true then 1 else 0) = ∑ x : Fin n → Bool, (∏ i : Fin n, if x i = true then p else 1 - p) * if f x ≠ f (flipBit x j) then 1 else 0

theorem BooleanFourier.russo_margulis {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) : HasDerivAt (pBiasedExpectation f) (∑ i : Fin n, pBiasedInfluence f i p) p