`phase_failure_cost_lower_bound`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.PhaseFailureCost
domain: NumberTheory
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.PhaseFailureCost on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  55/-- Packaged form using `GateFailureCost`. -/
  56theorem phase_failure_accumulates_packaged
  57    {n : ℕ} {S : Finset ℕ} {failure : ∀ c : ℕ, GateFailureCost n c}
  58    (hS : S.Nonempty)
  59    (hfails : ∀ c ∈ S, GateFails n c) :
  60    0 < cumulativeFailureCost n (fun c => (failure c).cost) S := by
  61  apply phase_failure_accumulates hS hfails
  62  intro c hc
  63  exact (failure c).positive_of_failure (hfails c hc)
  64
  65end PhaseFailureCost
  66end NumberTheory
  67end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.