OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedEstimatorExecution.ratioBlock line 18
2. def OAI.ContingencyTables.RootedEstimatorExecution.correctionBlock line 24
3. def OAI.ContingencyTables.RootedEstimatorExecution.data line 31
4. lemma OAI.ContingencyTables.RootedEstimatorExecution.ratioBlock_value line 38
5. lemma OAI.ContingencyTables.RootedEstimatorExecution.correctionBlock_value line 53
6. theorem OAI.ContingencyTables.RootedEstimatorExecution.output_data line 75

   Source documentation

   The actual list program returns the exact value of the transported finite experiment, including unsuccessful statistical outcomes.

   theorem output_data (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
       (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
       (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C) (delta failure : ℚ)
       (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
   …

   Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.RootedCatalogGrid.freeCount

7. lemma OAI.ContingencyTables.RootedEstimatorExecution.property_of_sameLaw line 100
8. theorem OAI.ContingencyTables.RootedEstimatorExecution.output_range line 127

   Source documentation

   Full finite support transfers the proved deterministic range to all physical sample words, not only to the high-probability event.

   theorem output_range (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
       (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
       (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C) (delta failure : ℚ)
       (hd0 : 0 < delta) (hd1 : delta < 1) (hf : 0 < failure)
       (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
   …

   Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.RootedCatalogGrid.freeCount

9. theorem OAI.ContingencyTables.RootedEstimatorExecution.output_failure line 148