noncomputable def BooleanFourier.correlatedPairProb (ρ : ℝ) (_hρ : ρ ∈ Set.Icc (-1) 1) (a b : Bool) : ℝ

noncomputable def BooleanFourier.correlatedProb {n : ℕ} (ρ : ℝ) (_hρ : ρ ∈ Set.Icc (-1) 1) (x y : Fin n → Bool) : ℝ

theorem BooleanFourier.correlatedProb_factor_nonneg {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (x y : Fin n → Bool) (i : Fin n) : 0 ≤ (1 + ρ * (boolToReal (x i) * boolToReal (y i))) / 2

theorem BooleanFourier.correlatedProb_factor_sum {n : ℕ} (ρ : ℝ) (x : Fin n → Bool) (i : Fin n) : ∑ b : Bool, (1 + ρ * (boolToReal (x i) * boolToReal b)) / 2 = 1

structure BooleanFourier.NoisyHypercube : Type

• n : ℕ
• ρ : ℝ
• hρ_nonneg : 0 ≤ self.ρ
• hρ_le_one : self.ρ ≤ 1

noncomputable def BooleanFourier.noisyHypercubeTransitionProb {n : ℕ} (ρ : ℝ) (_hρ₀ : 0 ≤ ρ) (_hρ₁ : ρ ≤ 1) (x y : Fin n → Bool) : ℝ

noncomputable def BooleanFourier.NoisyHypercube.transitionProb (G : NoisyHypercube) (x y : Fin G.n → Bool) : ℝ

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