OAI/Combinatorics/ContingencyTables/Counting/CompanionReferenceAccuracy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Relative accuracy of the literal companion ratio estimator

The source's tolerance epsilon/(200(H+1)) turns the proved accumulated logarithmic error into the required multiplicative error. The terminal contamination bound supplies the remaining error term.

  1. theorem OAI.ContingencyTables.CompanionReferenceAccuracy.relative_of_log_error line 17
  2. def OAI.ContingencyTables.CompanionReferenceAccuracy.tolerance line 34
  3. theorem OAI.ContingencyTables.CompanionReferenceAccuracy.accurate_phases_relative line 37
  4. theorem OAI.ContingencyTables.CompanionReferenceAccuracy.reference_accuracy line 63

    Source documentation

    The terminal contamination bound and a successful phase history give a relative-error estimate of the table count.

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

    Mentions: OAI.ContingencyTables.CompanionReferenceAccuracy.tolerance