OAI/Combinatorics/ContingencyTables/Transport/FiniteRationalThreshold.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FairBits.rationalThreshold line 16
2. def OAI.ContingencyTables.FairBits.rationalThresholdMass line 18
3. abbrev OAI.ContingencyTables.FairBits.rationalThresholdAccept line 20
4. lemma OAI.ContingencyTables.FairBits.rationalThreshold_le line 23
5. lemma OAI.ContingencyTables.FairBits.rationalThreshold_count line 31
6. theorem OAI.ContingencyTables.FairBits.rationalThreshold_error line 38

   Source documentation

   The finite coin always rounds downward and loses less than one code word, including the exact endpoint probabilities zero and one.

   theorem rationalThreshold_error (k : ℕ) (q : ℚ) (hq : 0 ≤ q) :
       0 ≤ rationalThresholdMass k q ∧ rationalThresholdMass k q ≤ q ∧
         q-rationalThresholdMass k q < 1/(2:ℚ)^k := by
   …

   Mentions: OAI.ContingencyTables.FairBits.rationalThresholdMass

7. theorem OAI.ContingencyTables.FairBits.rationalThreshold_expectation line 53

   Source documentation

   An actual k-bit input realizes the stated rounded probability.

   theorem rationalThreshold_expectation (k : ℕ) (q : ℚ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
       uniformAverage (fun bits : Fin k → Bool =>
         if rationalThresholdAccept k q bits then (1:ℝ) else 0)=
           (rationalThresholdMass k q:ℝ) := by
   …

   Mentions: OAI.ContingencyTables.FairBits.rationalThresholdAccept, OAI.ContingencyTables.FairBits.rationalThresholdMass