OAI/Combinatorics/ContingencyTables/Counting/CompanionTerminalApplication.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal finite phase estimator has the required counting accuracy

  1. def OAI.ContingencyTables.CompanionTerminalApplication.finalPhase line 17
  2. lemma OAI.ContingencyTables.CompanionTerminalApplication.final_parameter line 20
  3. theorem OAI.ContingencyTables.CompanionTerminalApplication.terminal_normalizer line 29
  4. theorem OAI.ContingencyTables.CompanionTerminalApplication.successful_history_accuracy line 46

    Source documentation

    Successful observations of the finite phase history estimate the original bounded-table count, with terminal contamination derived from the literal root/tree weights.

    theorem successful_history_accuracy (A : Instance I J) (E : Endpoints A)
    (samples : ℕ → List (Set (Labels A×Bool))) (L : ℕ) (epsilon : ℝ)
    (he : 0 < epsilon) (he1 : epsilon < 1)
    (hW : 20*A.d ≤ A.W) (hL : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^L)
    (hall : ∀ j < finalPhase A L epsilon,
      Accurate A samples (tolerance epsilon (finalPhase A L epsilon)) j) :
    (1-epsilon)*tableCount A ≤ estimate A samples (finalPhase A L epsilon) ∧
      estimate A samples (finalPhase A L epsilon) ≤ (1+epsilon)*tableCount A := by
…

    Mentions: OAI.ContingencyTables.CompanionTerminalApplication.finalPhase