OAI/Combinatorics/ContingencyTables/Rooted/RootedTerminalApplication.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedTerminalApplication.terminal_normalizer line 20
2. theorem OAI.ContingencyTables.RootedTerminalApplication.successful_history_accuracy line 37

   Source documentation

   Successful observations of the original 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) (R : RootedCompletion.Selection A.T) (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 R samples (tolerance epsilon (finalPhase A L epsilon)) j) :
       (1-epsilon)*tableCount A ≤ estimate A R samples (finalPhase A L epsilon) ∧
         estimate A R samples (finalPhase A L epsilon) ≤ (1+epsilon)*tableCount A := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection