OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.oracleProposalRat line 18
2. def OAI.ContingencyTables.CompanionOracleDensity.oracleMove line 20
3. def OAI.ContingencyTables.CompanionOracleDensity.oracleTransition line 25
4. lemma OAI.ContingencyTables.CompanionOracleDensity.oracleMove_cast line 29
5. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleTransition_cast line 39
6. def OAI.ContingencyTables.CompanionOracleDensity.oracleTransitionLaw line 48
7. def OAI.ContingencyTables.CompanionOracleDensity.oracleWalkLaw line 61
8. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleWalkLaw_cast line 66
9. def OAI.ContingencyTables.CompanionOracleDensity.oracleStationaryLaw line 81
10. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleStationaryLaw_cast line 91
11. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleWalkLaw_variation line 101

    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) (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.CompanionOracleDensity.height, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger