FairBits.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Bounded fair-bit scaling

Both papers for result 200 implement a bounded approximately uniform integer choice by drawing z uniformly from 0,...,Q-1 and returning ⌊M*z/Q⌋. When Q = 2^k, the input choice uses exactly k fair bits.

We prove the exact integer fiber formula in 200-01, equation eq:dense-offset-count, and the pointwise and total-variation error estimates used in 200-02, Lemma lem:dyadic-integer-draw. The arguments are direct finite arithmetic and have no published-input hypotheses.

def OAI.ContingencyTables.FairBits.scale line 29
Source documentation
The bounded scaling map on integer proposals.
```
def scale (M Q z : ℕ) : ℕ := ⌊(M : ℚ) * z / Q⌋₊
```
lemma OAI.ContingencyTables.FairBits.scale_eq_div line 32
Source documentation
The rational floor is exactly the implemented natural integer quotient.
```
lemma scale_eq_div (M Q z : ℕ) : scale M Q z = M * z / Q := by
…
```
Mentions: OAI.ContingencyTables.FairBits.scale
def OAI.ContingencyTables.FairBits.endpoint line 36
Source documentation
The first integer whose scaled value can be at least β.
```
def endpoint (M Q β : ℕ) : ℕ := ⌈(β : ℚ) * Q / M⌉₊
```
def OAI.ContingencyTables.FairBits.fiber line 39
Source documentation
The proposal integers that produce a given output.
```
def fiber (M Q β : ℕ) : Finset ℕ :=
…
```
lemma OAI.ContingencyTables.FairBits.scale_lt line 42
lemma OAI.ContingencyTables.FairBits.scale_eq_iff line 50
lemma OAI.ContingencyTables.FairBits.endpoint_le_proposal line 74
theorem OAI.ContingencyTables.FairBits.fiber_eq_interval line 83
Source documentation
The exact preimage interval, including both endpoint conventions.
```
theorem fiber_eq_interval {M Q β : ℕ} (hM : 0 < M) (hQ : 0 < Q)
    (hβ : β < M) :
    fiber M Q β = Finset.Ico (endpoint M Q β) (endpoint M Q (β + 1)) := by
…
```
Mentions: OAI.ContingencyTables.FairBits.fiber, OAI.ContingencyTables.FairBits.endpoint
theorem OAI.ContingencyTables.FairBits.fiber_card line 96
Source documentation
This is the ceiling-difference formula used to tabulate the implemented output law without enumerating all random bit strings.
```
theorem fiber_card {M Q β : ℕ} (hM : 0 < M) (hQ : 0 < Q) (hβ : β < M) :
    (fiber M Q β).card = endpoint M Q (β + 1) - endpoint M Q β := by
…
```
Mentions: OAI.ContingencyTables.FairBits.fiber, OAI.ContingencyTables.FairBits.endpoint
lemma OAI.ContingencyTables.FairBits.endpoint_mono line 100
theorem OAI.ContingencyTables.FairBits.fiber_card_error line 109
Source documentation
A scaled output has a number of preimages differing by less than one from the ideal real-valued number Q/M.
```
theorem fiber_card_error {M Q β : ℕ} (hM : 0 < M) (hQ : 0 < Q) (hβ : β < M) :
    |((fiber M Q β).card : ℚ) - (Q : ℚ) / M| < 1 := by
…
```
Mentions: OAI.ContingencyTables.FairBits.fiber
def OAI.ContingencyTables.FairBits.outputMass line 124
Source documentation
The exact mass assigned by the finite uniform proposal.
```
def outputMass (M Q β : ℕ) : ℚ := (fiber M Q β).card / (Q : ℚ)
```
Mentions: OAI.ContingencyTables.FairBits.fiber
lemma OAI.ContingencyTables.FairBits.outputMass_nonnegative line 126
theorem OAI.ContingencyTables.FairBits.outputMass_total line 131
Source documentation
The masses are normalized on the declared output range.
```
theorem outputMass_total {M Q : ℕ} (hM : 0 < M) (hQ : 0 < Q) :
    ∑ β ∈ Finset.range M, outputMass M Q β = 1 := by
…
```
Mentions: OAI.ContingencyTables.FairBits.outputMass
theorem OAI.ContingencyTables.FairBits.outputMass_error line 146
Source documentation
Every point mass differs from uniform by at most 1/Q.
```
theorem outputMass_error {M Q β : ℕ} (hM : 0 < M) (hQ : 0 < Q) (hβ : β < M) :
    |outputMass M Q β - 1 / (M : ℚ)| ≤ 1 / (Q : ℚ) := by
…
```
Mentions: OAI.ContingencyTables.FairBits.outputMass
def OAI.ContingencyTables.FairBits.variationFromUniform line 159
Source documentation
Total variation with the manuscript's convention ½ ∑ |p-u|.
```
def variationFromUniform (M Q : ℕ) : ℚ :=
…
```
theorem OAI.ContingencyTables.FairBits.variation_bound line 164
Source documentation
The bounded integer draw has total-variation error at most M/(2Q). The papers use the weaker bound M/Q.
```
theorem variation_bound {M Q : ℕ} (hM : 0 < M) (hQ : 0 < Q) :
    variationFromUniform M Q ≤ (M : ℚ) / (2 * Q) := by
…
```
Mentions: OAI.ContingencyTables.FairBits.variationFromUniform