OAI/Combinatorics/ContingencyTables/Counting/CountingBranchMachine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CountingBranchProgram.machine line 15
2. def OAI.ContingencyTables.CountingBranchProgram.machineTime line 17
3. def OAI.ContingencyTables.CountingBranchProgram.sourceValue line 20
4. lemma OAI.ContingencyTables.CountingBranchProgram.sourceValue_nonnegative line 23
5. lemma OAI.ContingencyTables.CountingBranchProgram.sourceValue_output line 26
6. theorem OAI.ContingencyTables.CountingBranchProgram.outputs_nonnegative line 34

   Source documentation

   Every random tape halts with a nonnegative rational, including on statistically unsuccessful histories of the positive-label branch.

   theorem outputs_nonnegative (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
       (epsilon delta : ℚ) (t : ℕ)
       (ht : machineTime positive F width N (Algorithms.encodeCountingInput r c b epsilon delta) ≤ t) :
       ∀ bits : Bits t, ∃ q : ℚ, 0 ≤ q ∧
         Outputs (machine positive F width N) (Algorithms.encodeCountingInput r c b epsilon delta) bits q := by
   …

   Mentions: OAI.ContingencyTables.CountingBranchProgram.machineTime, OAI.ContingencyTables.Algorithms.encodeCountingInput, OAI.ContingencyTables.CountingBranchProgram.machine

7. lemma OAI.ContingencyTables.CountingBranchProgram.sourceValue_zero line 50
8. theorem OAI.ContingencyTables.CountingBranchProgram.outputs_zero line 61

   Source documentation

   Exact zero output follows from the executed feasibility test.

   theorem outputs_zero (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
       (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ) (epsilon delta : ℚ)
       (hz : Algorithms.count r c b=0) (t : ℕ)
       (ht : machineTime positive F width N (Algorithms.encodeCountingInput r c b epsilon delta) ≤ t) :
       ∀ bits : Bits t,
         Outputs (machine positive F width N) (Algorithms.encodeCountingInput r c b epsilon delta) bits 0 := by
   …

   Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.Algorithms.count, OAI.ContingencyTables.CountingBranchProgram.machineTime, OAI.ContingencyTables.Algorithms.encodeCountingInput, OAI.ContingencyTables.CountingBranchProgram.machine