variance_const_zero

formal source

  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 : ℕ) :
  64    ∀ (a : Fin n → Bool) (k : Fin n),
  65      jcostEdgeWeight (⟨[], n, rfl⟩ : CNFFormula n) a k = 0 := by
  66  intro a k
  67  unfold jcostEdgeWeight satJCost; simp
  68
  69/-- UNSAT gap condition: structure for formulas where every edge has
  70    positive J-cost weight. -/
  71structure UNSATGapCondition (n : ℕ) (f : CNFFormula n) where
  72  is_unsat : f.isUNSAT