theorem BooleanFourier.sum_chi_mul_chi_point {n : ℕ} (S T : Finset (Fin n)) : ∑ x : Fin n → Bool, chi S x * chi T x = if S = T then 2 ^ n else 0

noncomputable def BooleanFourier.noiseOp {n : ℕ} (ρ : ℝ) (f : BoolFn n) : BoolFn n

theorem BooleanFourier.noise_kernel_expand {n : ℕ} (ρ : ℝ) (x y : Fin n → Bool) : ∏ i : Fin n, (1 + ρ * boolToReal (x i) * boolToReal (y i)) = ∑ S : Finset (Fin n), ρ ^ S.card * chi S x * chi S y

theorem BooleanFourier.noiseOp_eq_fourier_expansion {n : ℕ} (ρ : ℝ) (f : BoolFn n) (x : Fin n → Bool) : noiseOp ρ f x = ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S * chi S x

theorem BooleanFourier.noiseOp_fourierCoeff {n : ℕ} (ρ : ℝ) (f : BoolFn n) (S : Finset (Fin n)) : fourierCoeff (noiseOp ρ f) S = ρ ^ S.card * fourierCoeff f S

theorem BooleanFourier.noiseOp_l2_norm_sq {n : ℕ} (ρ : ℝ) (f : BoolFn n) : ∑ S : Finset (Fin n), fourierCoeff (noiseOp ρ f) S ^ 2 = ∑ S : Finset (Fin n), ρ ^ (2 * S.card) * fourierCoeff f S ^ 2

noncomputable def BooleanFourier.restrictLast {n : ℕ} (f : BoolFn (n + 1)) (b : Bool) : BoolFn n

theorem BooleanFourier.sum_finBool_succ_split {n : ℕ} (g : (Fin (n + 1) → Bool) → ℝ) : ∑ x : Fin (n + 1) → Bool, g x = ∑ x' : Fin n → Bool, g (Fin.snoc x' true) + ∑ x' : Fin n → Bool, g (Fin.snoc x' false)

theorem BooleanFourier.lpNorm_restrictLast {n : ℕ} (f : BoolFn (n + 1)) {q : ℝ} (hq : 0 < q) : lpNorm q f ^ q = 1 / 2 * lpNorm q (restrictLast f true) ^ q + 1 / 2 * lpNorm q (restrictLast f false) ^ q

theorem BooleanFourier.fourierCoeff_restrictLast {n : ℕ} (f : BoolFn (n + 1)) (b : Bool) (T : Finset (Fin n)) : fourierCoeff (restrictLast f b) T = fourierCoeff f (Finset.map Fin.castSuccEmb T) + boolToReal b * fourierCoeff f (Finset.map Fin.castSuccEmb T ∪ {Fin.last n})

theorem BooleanFourier.noiseOp_one {n : ℕ} (f : BoolFn n) : noiseOp 1 f = f

theorem BooleanFourier.noiseOp_comp {n : ℕ} (ρ σ : ℝ) (f : BoolFn n) : noiseOp ρ (noiseOp σ f) = noiseOp (ρ * σ) f

theorem BooleanFourier.sum_pow_card_mul_fourierCoeff_sq_le {n : ℕ} (f : BoolFn n) (k : ℕ) (c : ℝ) (hc : 1 ≤ c) (hdeg : degree f ≤ k) : ∑ S : Finset (Fin n), c ^ S.card * fourierCoeff f S ^ 2 ≤ c ^ k * ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

theorem BooleanFourier.hypercontractive_low_degree {n : ℕ} (f : BoolFn n) (k : ℕ) (q : ℝ) (hq : 2 ≤ q) (hdeg : degree f ≤ k) (h_bb : ∀ (g : BoolFn n) (ρ' : ℝ), 0 ≤ ρ' → ρ' ≤ √((2 - 1) / (q - 1)) → lpNorm q (noiseOp ρ' g) ≤ lpNorm 2 g) : lpNorm q f ≤ (q - 1) ^ (↑k / 2) * lpNorm 2 f

theorem BooleanFourier.fourierCoeff_noiseOp {n : ℕ} (ρ : ℝ) (f : BoolFn n) (S : Finset (Fin n)) : fourierCoeff (noiseOp ρ f) S = ρ ^ S.card * fourierCoeff f S

noncomputable def BooleanFourier.combineAssignment {n : ℕ} (J : Finset (Fin n)) (xJ : ↥J → Bool) (z : ↥Jᶜ → Bool) : Fin n → Bool

noncomputable def BooleanFourier.restrictToSubset {n : ℕ} (J : Finset (Fin n)) (f : BoolFn n) (z : ↥Jᶜ → Bool) : (↥J → Bool) → ℝ

noncomputable def BooleanFourier.chiOn {n : ℕ} (J : Finset (Fin n)) (S : Finset ↥J) (x : ↥J → Bool) : ℝ

noncomputable def BooleanFourier.fourierCoeffOn {n : ℕ} (J : Finset (Fin n)) (g : (↥J → Bool) → ℝ) (S : Finset ↥J) : ℝ

theorem BooleanFourier.subtype_map_union_left {n : ℕ} (J : Finset (Fin n)) (S : Finset ↥J) (T : Finset ↥Jᶜ) : Finset.subtype (fun (x : Fin n) => x ∈ J) (Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ J) S ∪ Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ Jᶜ) T) = S

theorem BooleanFourier.subtype_map_union_right {n : ℕ} (J : Finset (Fin n)) (S : Finset ↥J) (T : Finset ↥Jᶜ) : Finset.subtype (fun (x : Fin n) => x ∈ Jᶜ) (Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ J) S ∪ Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ Jᶜ) T) = T

theorem BooleanFourier.finset_subtype_map_union {n : ℕ} (J U : Finset (Fin n)) : U = Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ J) (Finset.subtype (fun (x : Fin n) => x ∈ J) U) ∪ Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ Jᶜ) (Finset.subtype (fun (x : Fin n) => x ∈ Jᶜ) U)

theorem BooleanFourier.chi_combineAssignment_eq {n : ℕ} (J U : Finset (Fin n)) (xJ : ↥J → Bool) (z : ↥Jᶜ → Bool) : chi U (combineAssignment J xJ z) = chiOn J (Finset.subtype (fun (x : Fin n) => x ∈ J) U) xJ * chiOn Jᶜ (Finset.subtype (fun (x : Fin n) => x ∈ Jᶜ) U) z

theorem BooleanFourier.sum_chiOn_mul_chiOn {n : ℕ} (J : Finset (Fin n)) (S T : Finset ↥J) : ∑ x : ↥J → Bool, chiOn J S x * chiOn J T x = if S = T then 2 ^ J.card else 0

theorem BooleanFourier.fourierCoeff_restrictToSubset {n : ℕ} (J : Finset (Fin n)) (f : BoolFn n) (z : ↥Jᶜ → Bool) (S : Finset ↥J) : fourierCoeffOn J (restrictToSubset J f z) S = ∑ T : Finset ↥Jᶜ, fourierCoeff f (Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ J) S ∪ Finset.map (Function.Embedding.subtype fun (x : Fin n) => x ∈ Jᶜ) T) * chiOn Jᶜ T z