theorem hastad_tssw (ε : ℝ) : ε > 0 → MaxCut.IsNPHardGapMaxCut 1 (16 / 17 + ε)

noncomputable def Hardness.dinurSafraConstant : ℝ

def Hardness.IsPolyTimeComputable {numVerts : ℕ → ℕ} : ((m : ℕ) → PCP.BinaryString m → SimpleGraph (Fin (numVerts m))) → Prop

def Hardness.IsPolyTimeVertexCoverReduction {numVerts : ℕ → ℕ} (reduce : (m : ℕ) → PCP.BinaryString m → SimpleGraph (Fin (numVerts m))) : Prop

def Hardness.IsNPHardToApproximateVertexCover (α : ℝ) : Prop

theorem Hardness.dinur_safra_vertex_cover : IsNPHardToApproximateVertexCover dinurSafraConstant

theorem BooleanFourier.sheppard_halfspace_stability {n : ℕ} {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_le : ρ ≤ 1) (hn : 0 < n) : (GaussianStability.gaussianNoiseStability ρ hρ_nonneg hρ_le fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1) = 2 / Real.pi * Real.arcsin ρ

theorem BooleanFourier.gaussianNoiseOperator_monomial {n : ℕ} (ρ : ℝ) (S : Finset (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : ∫ (w : EuclideanSpace ℝ (Fin n)), ∏ i ∈ S, (ρ • x + √(1 - ρ ^ 2) • w).ofLp i ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = ρ ^ S.card * ∏ i ∈ S, x.ofLp i

theorem BooleanFourier.integral_sq_gaussianReal : ∫ (x : ℝ), x ^ 2 ∂ProbabilityTheory.gaussianReal 0 1 = 1

theorem BooleanFourier.coord_integral_factor {n : ℕ} (S T : Finset (Fin n)) (k : Fin n) : ∫ (t : ℝ), (if k ∈ S then t else 1) * if k ∈ T then t else 1 ∂ProbabilityTheory.gaussianReal 0 1 = if k ∈ S ∧ k ∈ T then 1 else if k ∈ S ∨ k ∈ T then 0 else 1

theorem BooleanFourier.prod_coord_factors_eq {n : ℕ} (S T : Finset (Fin n)) : (∏ k : Fin n, if k ∈ S ∧ k ∈ T then 1 else if k ∈ S ∨ k ∈ T then 0 else 1) = if S = T then 1 else 0

theorem BooleanFourier.integral_monomial_mul_monomial_stdGaussian {n : ℕ} (S T : Finset (Fin n)) : ∫ (x : EuclideanSpace ℝ (Fin n)), (∏ i ∈ S, x.ofLp i) * ∏ j ∈ T, x.ofLp j ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = if S = T then 1 else 0

theorem BooleanFourier.integrable_monomial_noise_pi {n : ℕ} (S : Finset (Fin n)) (ρ : ℝ) (x : EuclideanSpace ℝ (Fin n)) : MeasureTheory.Integrable (fun (w : Fin n → ℝ) => ∏ i ∈ S, (ρ * x.ofLp i + √(1 - ρ ^ 2) * w i)) (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 1)

theorem BooleanFourier.integrable_monomial_noise_stdGaussian {n : ℕ} (S : Finset (Fin n)) (ρ : ℝ) (x : EuclideanSpace ℝ (Fin n)) : MeasureTheory.Integrable (fun (w : EuclideanSpace ℝ (Fin n)) => ∏ i ∈ S, (ρ • x + √(1 - ρ ^ 2) • w).ofLp i) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)))

theorem BooleanFourier.noiseStability_eq_gaussianNoiseStability_multilinear {n : ℕ} {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_lt : ρ < 1) (f : (Fin n → Bool) → ℝ) (hbv : IsBooleanValued f) (hbal : IsBalanced f) : noiseStability ρ f = GaussianStability.gaussianNoiseStability ρ hρ_nonneg ⋯ fun (x : EuclideanSpace ℝ (Fin n)) => multilinearExtension f fun (i : Fin n) => x.ofLp i

theorem BooleanFourier.multilinearExtension_gaussianStability_le_arcsin {n : ℕ} (f : (Fin n → Bool) → ℝ) (hbv : IsBooleanValued f) (hbal : IsBalanced f) {τ : ℝ} (hτ_pos : 0 < τ) (hinf : ∀ (i : Fin n), fourierInfluence f i ≤ τ) (ρ : ℝ) (hρ_nonneg : 0 ≤ ρ) (hρ_le : ρ ≤ 1) (hρ_lt : ρ < 1) : (GaussianStability.gaussianNoiseStability ρ hρ_nonneg hρ_le fun (x : EuclideanSpace ℝ (Fin n)) => multilinearExtension f fun (i : Fin n) => x.ofLp i) ≤ 2 / Real.pi * Real.arcsin ρ + 2 / (1 - ρ) * √τ

theorem BooleanFourier.multilinearExtension_integral_stdGaussian_eq_zero {n : ℕ} (f : (Fin n → Bool) → ℝ) (hbal : IsBalanced f) : ∫ (x : EuclideanSpace ℝ (Fin n)), multilinearExtension f fun (i : Fin n) => x.ofLp i ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0

theorem BooleanFourier.multilinearExtension_bounded_on_cube {n : ℕ} (f : (Fin n → Bool) → ℝ) (hbv : IsBooleanValued f) (x : Fin n → ℝ) (hx : ∀ (i : Fin n), x i ∈ Set.Icc (-1) 1) : multilinearExtension f x ∈ Set.Icc (-1) 1

theorem BooleanFourier.multilinearExtension_satisfies_borell_hypotheses {n : ℕ} (f : (Fin n → Bool) → ℝ) (hbv : IsBooleanValued f) (hbal : IsBalanced f) : (∀ (x : Fin n → ℝ), (∀ (i : Fin n), x i ∈ Set.Icc (-1) 1) → multilinearExtension f x ∈ Set.Icc (-1) 1) ∧ ∫ (x : EuclideanSpace ℝ (Fin n)), multilinearExtension f fun (i : Fin n) => x.ofLp i ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0

theorem BooleanFourier.noise_stability_lindeberg_bound {n : ℕ} {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_lt : ρ < 1) (hn : 0 < n) (f : (Fin n → Bool) → ℝ) (hbv : IsBooleanValued f) (hbal : IsBalanced f) {τ : ℝ} (hτ_pos : 0 < τ) (hinf : ∀ (i : Fin n), fourierInfluence f i ≤ τ) : noiseStability ρ f ≤ (GaussianStability.gaussianNoiseStability ρ hρ_nonneg ⋯ fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1) + 2 / (1 - ρ) * √τ

theorem BooleanFourier.invariance_principle_gaussian_bound {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_lt : ρ < 1) {δ : ℝ} (hδ : 0 < δ) : ∃ τ > 0, ∀ {n : ℕ} (hn : 0 < n) (f : (Fin n → Bool) → ℝ), IsBooleanValued f → IsBalanced f → (∀ (i : Fin n), fourierInfluence f i ≤ τ) → noiseStability ρ f ≤ (GaussianStability.gaussianNoiseStability ρ hρ_nonneg ⋯ fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1) + δ

theorem BooleanFourier.majority_is_stablest {ρ : ℝ} (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) {ε : ℝ} (hε : 0 < ε) : ∃ τ > 0, ∀ {n : ℕ} (f : (Fin n → Bool) → ℝ), IsBooleanValued f → IsBalanced f → (∀ (i : Fin n), fourierInfluence f i ≤ τ) → noiseStability ρ f ≤ 2 / Real.pi * Real.arcsin ρ + ε

noncomputable def BooleanFourier.lowDegreePart {n : ℕ} (d : ℕ) (f : (Fin n → Bool) → ℝ) (x : Fin n → Bool) : ℝ

theorem BooleanFourier.majority_is_stablest_real_valued {ε : ℝ} (hε : 0 < ε) {ρ : ℝ} (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) : ∃ (d : ℕ), ∃ τ > 0, ∀ {n : ℕ} (f : (Fin n → Bool) → ℝ), (∀ (x : Fin n → Bool), f x ∈ Set.Icc (-1) 1) → IsBalanced f → (∀ (i : Fin n), influenceReal (lowDegreePart d f) i ≤ τ) → noiseStability ρ f ≤ 1 - 2 / Real.pi * Real.arccos ρ + ε