GateFailureCost

formal source

  21
  22/-- An abstract cost assignment for a failed gate.  The positivity field is
  23the only property needed for the finite accumulation theorems. -/
  24structure GateFailureCost (n c : ℕ) where
  25  cost : ℝ
  26  positive_of_failure : GateFails n c → 0 < cost
  27
  28/-- Cumulative unresolved phase cost over a finite gate set. -/
  29def cumulativeFailureCost (_n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) : ℝ :=
  30  S.sum costOf
  31
  32/-- If every gate in a nonempty finite set fails and each failed gate has
  33positive cost, then the cumulative cost is positive. -/
  34theorem phase_failure_accumulates
  35    {n : ℕ} {S : Finset ℕ} {costOf : ℕ → ℝ}
  36    (hS : S.Nonempty)
  37    (_hfails : ∀ c ∈ S, GateFails n c)
  38    (hpos : ∀ c ∈ S, 0 < costOf c) :
  39    0 < cumulativeFailureCost n costOf S := by
  40  unfold cumulativeFailureCost
  41  exact Finset.sum_pos hpos hS
  42
  43/-- Lower bound: if every failed gate in `S` costs at least `δ`, then the
  44total unresolved phase cost is at least `δ * S.card`. -/
  45theorem phase_failure_cost_lower_bound
  46    {n : ℕ} {S : Finset ℕ} {costOf : ℕ → ℝ} {δ : ℝ}
  47    (_hfails : ∀ c ∈ S, GateFails n c)
  48    (hlower : ∀ c ∈ S, δ ≤ costOf c) :
  49    δ * (S.card : ℝ) ≤ cumulativeFailureCost n costOf S := by
  50  unfold cumulativeFailureCost
  51  calc
  52    δ * (S.card : ℝ) = S.sum (fun _ => δ) := by simp; ring
  53    _ ≤ S.sum costOf := Finset.sum_le_sum hlower
  54