OAI/Combinatorics/ContingencyTables/Rooted/RootedStoredHistory.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Stored rational outputs of the actual outer phases

The initial record is at index zero. Later records are the outputs stored in the finite history; the initial record also supplies every unused future entry to the restart's multiplier function.

  1. def OAI.ContingencyTables.RootedStoredHistory.lookup line 26
  2. lemma OAI.ContingencyTables.RootedStoredHistory.lookup_snoc_old line 30
  3. lemma OAI.ContingencyTables.RootedStoredHistory.lookup_snoc_new line 37
  4. lemma OAI.ContingencyTables.RootedStoredHistory.lookup_future line 42
  5. def OAI.ContingencyTables.RootedStoredHistory.Good line 48
  6. lemma OAI.ContingencyTables.RootedStoredHistory.good_nil line 53
  7. lemma OAI.ContingencyTables.RootedStoredHistory.good_snoc line 58
  8. lemma OAI.ContingencyTables.RootedStoredHistory.good_positive line 86
  9. lemma OAI.ContingencyTables.RootedStoredHistory.good_multipliers line 99
  10. theorem OAI.ContingencyTables.RootedStoredHistory.count_accuracy line 110

    Source documentation

    The rational value actually stored at the terminal history index has the counting guarantee whenever every executed update is valid.

    theorem count_accuracy (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (E : Endpoints A) (L : ℕ) (epsilon : ℝ) (he0 : 0 < epsilon) (he1 : epsilon < 1)
    (hW : 20*A.d ≤ A.W) (hL : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^L)
    (xi : ℚ) (eta : ℝ)
    (herr : (finalPhase A L epsilon:ℝ)*(4*(xi:ℝ)+4*eta) ≤ epsilon/50)
    (history : List (Stored A)) (hlen : history.length=finalPhase A L epsilon)
    (hg : Good A R xi eta history) :
    (1-epsilon)*tableCount A ≤ ((lookup A history history.length).estimate:ℝ) ∧
      ((lookup A history history.length).estimate:ℝ) ≤ (1+epsilon)*tableCount A := by
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedStoredHistory.Good, OAI.ContingencyTables.RootedStoredHistory.lookup