OAI/Combinatorics/ContingencyTables/Transport/BoundedOffsetLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FairBits.scaledLaw line 14
2. def OAI.ContingencyTables.FairBits.uniformIntLaw line 21
3. theorem OAI.ContingencyTables.FairBits.scaledLaw_variation line 28
4. def OAI.ContingencyTables.FairBits.offsetBitLength line 40
5. theorem OAI.ContingencyTables.FairBits.dense_scaled_offset_variation line 44

   Source documentation

   This law is the exact output law of multiplying the finite fair-bit integer by w and taking the integer quotient.

   theorem dense_scaled_offset_variation (w h d : ℕ) (hw : 0 < w) :
       variation (scaledLaw w (offsetBitLength w h d) hw) (uniformIntLaw w hw) ≤
         1 / (2 : ℚ) ^ (4 * (h + d)) := by
   …

   Mentions: OAI.ContingencyTables.FairBits.scaledLaw, OAI.ContingencyTables.FairBits.offsetBitLength, OAI.ContingencyTables.FairBits.uniformIntLaw

6. theorem OAI.ContingencyTables.FairBits.dense_offset_product_variation line 58