structure BooleanAnalysis.WeightedRegularGraph (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

• weight : V → V → ℝ
• degree : ℝ
• weight_nonneg (x y : V) : 0 ≤ self.weight x y
• degree_pos : 0 < self.degree
• regular (x : V) : ∑ y : V, self.weight x y = self.degree

noncomputable def BooleanAnalysis.WeightedRegularGraph.edgeExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (G : WeightedRegularGraph V) (S : Finset V) : ℝ

theorem BooleanAnalysis.WeightedRegularGraph.edgeExpansion_empty {V : Type u_1} [Fintype V] [DecidableEq V] (G : WeightedRegularGraph V) : G.edgeExpansion ∅ = 0

theorem BooleanAnalysis.WeightedRegularGraph.edgeExpansion_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : WeightedRegularGraph V) (S : Finset V) : 0 ≤ G.edgeExpansion S

def BooleanAnalysis.flip {n : ℕ} (x : Fin n → Bool) (i : Fin n) : Fin n → Bool

@[simp]

theorem BooleanAnalysis.flip_apply_same {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flip x i i = !x i

@[simp]

theorem BooleanAnalysis.flip_apply_ne {n : ℕ} (x : Fin n → Bool) (i j : Fin n) (h : j ≠ i) : flip x i j = x j

theorem BooleanAnalysis.flip_injective {n : ℕ} (x : Fin n → Bool) : Function.Injective (flip x)

noncomputable def BooleanAnalysis.edgeExpansion (n : ℕ) (A : Finset (Fin n → Bool)) : ℝ

theorem BooleanAnalysis.edgeExpansion_nonneg (n : ℕ) (A : Finset (Fin n → Bool)) : 0 ≤ edgeExpansion n A

@[simp]

theorem BooleanAnalysis.edgeExpansion_empty (n : ℕ) : edgeExpansion n ∅ = 0

noncomputable def BooleanAnalysis.edgeBoundaryMeasure (n : ℕ) (A : Finset (Fin n → Bool)) : ℝ

theorem BooleanAnalysis.edgeBoundaryMeasure_def {n : ℕ} (hn : n ≠ 0) (A : Finset (Fin n → Bool)) : edgeBoundaryMeasure n A = ↑{p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ flip p.1 p.2 ∉ A ∨ p.1 ∉ A ∧ flip p.1 p.2 ∈ A}.card / (↑n * 2 ^ n)