RootedReferenceAccuracy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selected-root phase estimates have the required relative accuracy

theorem OAI.ContingencyTables.RootedReferenceAccuracy.accurate_phases_relative line 16

theorem OAI.ContingencyTables.RootedReferenceAccuracy.reference_accuracy line 42

Source documentation

Once the separately proved terminal contamination estimate is available, the successful actual phase history estimates the table count.

theorem reference_accuracy (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (samples : ℕ → List (Set (Labels A×Bool))) (epsilon Z : ℝ)
    (he0 : 0 < epsilon) (he1 : epsilon < 1) (hZ : 0 ≤ Z) (H : ℕ)
    (hall : ∀ j < H, Accurate A R samples (tolerance epsilon H) j)
    (hterminal : Z ≤ total A R H ∧ total A R H ≤ (1+epsilon/32)*Z) :
    (1-epsilon)*Z ≤ estimate A R samples H ∧ estimate A R samples H ≤ (1+epsilon)*Z := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection