OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleDraw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.binSize_le_range line 19
2. abbrev OAI.ContingencyTables.CompanionOracleDensity.BinWords line 30
3. def OAI.ContingencyTables.CompanionOracleDensity.binWordBits line 33
4. def OAI.ContingencyTables.CompanionOracleDensity.binWordEquiv line 36
5. lemma OAI.ContingencyTables.CompanionOracleDensity.binBits_le line 40
6. def OAI.ContingencyTables.CompanionOracleDensity.binWordDraw line 48
7. theorem OAI.ContingencyTables.CompanionOracleDensity.binWordDraw_law line 57

   Source documentation

   The bin-dependent interval length only chooses a prefix of the fixed per-coordinate word. This preserves the analyzed quotient law.

   theorem binWordDraw_law (A : Instance I J) (K : ℕ) (hK : 0 < K) (hW : 100*A.d*K ≤ A.W)
       (v : Grid (I := Fin (dimension A)) K) (h : ℕ) :
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.dimension

8. def OAI.ContingencyTables.CompanionOracleDensity.flatBinDraw line 74
9. lemma OAI.ContingencyTables.CompanionOracleDensity.flatBinDraw_law line 78
10. def OAI.ContingencyTables.CompanionOracleDensity.stationaryIntegerLaw line 85
11. theorem OAI.ContingencyTables.CompanionOracleDensity.stationaryIntegerLaw_cast line 91

    Source documentation

    The stationary bin draw followed by the actual uniform integer interval draw is precisely the corrected mass used in the exact h identity.

    theorem stationaryIntegerLaw_cast (A : Instance I J) (C a : ℕ) (z : View A → ℕ)
        (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (f : FreeIndex A.small A.T A.b) :
        ((stationaryIntegerLaw A C a z K hK hW).mass f:ℝ)=correctedMass A C a z K (by omega) f := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.stationaryIntegerLaw, OAI.ContingencyTables.CompanionOracleDensity.correctedMass

12. def OAI.ContingencyTables.CompanionOracleDensity.sampledIntegerLaw line 107
13. theorem OAI.ContingencyTables.CompanionOracleDensity.sampledIntegerLaw_variation line 114

    Source documentation

    Both errors are accounted for once: mixing of the actual bin walk, then bounded quotient sampling inside its selected bin.

    theorem sampledIntegerLaw_variation (A : Instance I J) (C a : ℕ) (theta : ℝ)
        (hC : 0 < C) (haH : a ≤ rationalHeight A C) (htheta : 0 < theta)
        (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        (K Q h : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hW : 100*A.d*K ≤ A.W)
        (hKB : (K:ℝ) ≤ binWidth A C)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

14. lemma OAI.ContingencyTables.CompanionOracleDensity.map_product_bind line 135
15. def OAI.ContingencyTables.CompanionOracleDensity.oracleWalkWordEquiv line 159
16. def OAI.ContingencyTables.CompanionOracleDensity.flatOracleWalk line 162
17. lemma OAI.ContingencyTables.CompanionOracleDensity.flatOracleWalk_law line 167
18. def OAI.ContingencyTables.CompanionOracleDensity.oracleIntegerBits line 175
19. def OAI.ContingencyTables.CompanionOracleDensity.oracleIntegerDraw line 178
20. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleIntegerDraw_law line 187

    Source documentation

    One fixed Boolean word drives the bin walk and then the integer draw. The bin-dependent interval length never changes the reserved word length.

    theorem oracleIntegerDraw_law (A : Instance I J) (C a : ℕ) (z : View A → ℕ)
        (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
        (v : Grid (I := Fin (dimension A)) K) (n h : ℕ) :
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.dimension