OAI/Combinatorics/ContingencyTables/Counting/CompanionBinIntervals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.intervalSize line 18
2. def OAI.ContingencyTables.CompanionOracleDensity.intervalEquiv line 23

   Source documentation

   Each offset is sent to its integer by adding the exact lower ceiling endpoint. This is the actual source interval, not a cardinality-only choice.

   def intervalEquiv (K N beta : ℕ) (hK : 0 < K) (hN : 0 < N) (hb : beta < K) :
       Fin (intervalSize K N beta) ≃ {z : ℕ // z∈FairBits.fiber K N beta} where
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.intervalSize, OAI.ContingencyTables.FairBits.fiber

3. def OAI.ContingencyTables.CompanionOracleDensity.binSize line 45
4. theorem OAI.ContingencyTables.CompanionOracleDensity.binSize_positive line 49
5. def OAI.ContingencyTables.CompanionOracleDensity.binOffsetsEquiv line 62
6. def OAI.ContingencyTables.CompanionOracleDensity.binOffsetValue line 71
7. lemma OAI.ContingencyTables.CompanionOracleDensity.binOffsetValue_mem line 76
8. def OAI.ContingencyTables.CompanionOracleDensity.exactBinLaw line 81
9. def OAI.ContingencyTables.CompanionOracleDensity.approximateBinLaw line 86
10. theorem OAI.ContingencyTables.CompanionOracleDensity.exactBinLaw_mass line 92
11. theorem OAI.ContingencyTables.CompanionOracleDensity.approximateBinLaw_variation line 135

    Source documentation

    The explicitly shifted bounded quotient draws have a uniform error bound for every bin, including the case of no free coordinates.

    theorem approximateBinLaw_variation (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