CompanionOracleFiniteStep.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite Boolean experiment for each actual evaluator transition

lemma OAI.ContingencyTables.CompanionOracleDensity.oracle_acceptance_finite_coin line 20
def OAI.ContingencyTables.CompanionOracleDensity.finiteOracleStepLaw line 31
theorem OAI.ContingencyTables.CompanionOracleDensity.finiteOracleStepLaw_eq line 39
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) (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.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.dimension
def OAI.ContingencyTables.CompanionOracleDensity.oracleStepBits line 64
def OAI.ContingencyTables.CompanionOracleDensity.oracleBitStep line 67
def OAI.ContingencyTables.CompanionOracleDensity.oracleBitStepLaw line 76
lemma OAI.ContingencyTables.CompanionOracleDensity.oracleBitStepLaw_eq_finite line 80
theorem OAI.ContingencyTables.CompanionOracleDensity.oracleBitStepLaw_eq line 101
def OAI.ContingencyTables.CompanionOracleDensity.oracleBitWalkLaw line 109
theorem OAI.ContingencyTables.CompanionOracleDensity.oracleBitWalkLaw_eq line 115
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) (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.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.dimension
theorem OAI.ContingencyTables.CompanionOracleDensity.oracleBitWalkLaw_variation line 129