OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleFiniteStep.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedOracleDensity.oracle_acceptance_finite_coin line 17
2. def OAI.ContingencyTables.RootedOracleDensity.finiteOracleStepLaw line 28
3. theorem OAI.ContingencyTables.RootedOracleDensity.finiteOracleStepLaw_eq line 36

   Source documentation

   Every valid direction has one code; unused directions, boundary proposals and failed dyadic tests stay at the starting vertex.

   theorem finiteOracleStepLaw_eq (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (hC : 0 < C)
       (haH : a ≤ rationalHeight A C) (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
       {K : ℕ} (hK : 1 ≤ K) (hKB : (K:ℝ) ≤ binWidth A C)
       (v : Grid (I := Fin (dimension A)) K) :
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox

4. def OAI.ContingencyTables.RootedOracleDensity.oracleBitStep line 61
5. def OAI.ContingencyTables.RootedOracleDensity.oracleBitStepLaw line 70
6. lemma OAI.ContingencyTables.RootedOracleDensity.oracleBitStepLaw_eq_finite line 74
7. theorem OAI.ContingencyTables.RootedOracleDensity.oracleBitStepLaw_eq line 95
8. def OAI.ContingencyTables.RootedOracleDensity.oracleBitWalkLaw line 103
9. theorem OAI.ContingencyTables.RootedOracleDensity.oracleBitWalkLaw_eq line 109

   Source documentation

   A fixed rectangular Boolean array realizes the complete independent finite walk whose mixing estimate was proved for the real chain.

   theorem oracleBitWalkLaw_eq (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (hC : 0 < C)
       (haH : a ≤ rationalHeight A C) (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
       {K : ℕ} (hK : 1 ≤ K) (hKB : (K:ℝ) ≤ binWidth A C)
       (v : Grid (I := Fin (dimension A)) K) (n : ℕ) :
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox

10. theorem OAI.ContingencyTables.RootedOracleDensity.oracleBitWalkLaw_variation line 123