OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedOracleDensity.gridExponent_upper line 18
2. lemma OAI.ContingencyTables.RootedOracleDensity.rationalGridWeight_positive line 43
3. def OAI.ContingencyTables.RootedOracleDensity.oracleMove line 47
4. def OAI.ContingencyTables.RootedOracleDensity.oracleTransition line 52
5. lemma OAI.ContingencyTables.RootedOracleDensity.oracleMove_cast line 56
6. theorem OAI.ContingencyTables.RootedOracleDensity.oracleTransition_cast line 66
7. def OAI.ContingencyTables.RootedOracleDensity.oracleTransitionLaw line 75
8. def OAI.ContingencyTables.RootedOracleDensity.oracleWalkLaw line 88
9. theorem OAI.ContingencyTables.RootedOracleDensity.oracleWalkLaw_cast line 93
10. def OAI.ContingencyTables.RootedOracleDensity.oracleStationaryLaw line 108
11. theorem OAI.ContingencyTables.RootedOracleDensity.oracleStationaryLaw_cast line 118
12. theorem OAI.ContingencyTables.RootedOracleDensity.oracleWalkLaw_variation line 128

    Source documentation

    The rational finite-walk law inherits the proved source schedule. No exact real-valued primitive is used to define its transitions.

    theorem oracleWalkLaw_variation (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (theta : ℝ)
        (hC : 0 < C) (haH : (a:ℝ) ≤ height A C) (htheta : 0 < theta)
        (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        (K Q : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hKB : (K:ℝ) ≤ binWidth A C)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger