Variance

formal source

  30/-! ## Variance on the Boolean Hypercube -/
  31
  32/-- The variance of a real-valued function on {0,1}^n. -/
  33def Variance {n : ℕ} (x : (Fin n → Bool) → ℝ) : ℝ :=
  34  Finset.univ.sum (fun a : Fin n → Bool =>
  35    (x a - Finset.univ.sum (fun b : Fin n → Bool => x b) /
  36           (Finset.univ.card (α := Fin n → Bool) : ℝ))^2)
  37
  38theorem variance_nonneg {n : ℕ} (x : (Fin n → Bool) → ℝ) :
  39    0 ≤ Variance x :=
  40  Finset.sum_nonneg (fun a _ => sq_nonneg _)
  41
  42theorem variance_const_zero {n : ℕ} (c : ℝ) :
  43    Variance (fun _ : Fin n → Bool => c) = 0 := by
  44  unfold Variance; simp [sub_self, sq]
  45
  46/-! ## Convergence Rate -/
  47
  48/-- A convergence rate for iterative cost reduction on the J-cost landscape. -/
  49structure ConvergenceRate (n : ℕ) where
  50  rate : ℝ
  51  rate_lt_one : rate < 1
  52  rate_nonneg : 0 ≤ rate
  53
  54/-- The number of iterations needed to reduce cost below ε. -/
  55theorem iteration_bound_from_clauses {n : ℕ} (f : CNFFormula n)
  56    (gap : ℝ) (hgap : 0 < gap) :
  57    ∃ iters : ℕ, (iters : ℝ) ≥ f.clauses.length / gap :=
  58  ⟨Nat.ceil (↑f.clauses.length / gap), Nat.le_ceil _⟩
  59
  60/-! ## Landscape Properties -/
  61
  62/-- The empty formula has a flat landscape (all edge weights zero). -/
  63theorem empty_formula_flat_landscape (n : ℕ) :