BitEncoding.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Exact finite jitter encoding

For Q = 2^B, the integer code ⌊(r Q + j)/s⌋, with j uniform in {0,…,Q-1}, has exactly the distribution of the first B binary digits of (r + U)/s for uniform U in [0,1). This finite construction avoids continuous auxiliary probability spaces. Jointly uniform residue and jitter give a uniform code. Decoding can fail for at most s jitter values at each fixed residue, giving the stronger bound s/Q.

def OAI.TwoPointCorrelations.jitterPermutation line 26
Source documentation
Regroup the s Q equally likely elementary outcomes into Q blocks of size s.
```
def jitterPermutation (s Q : ℕ) : Fin s × Fin Q ≃ Fin Q × Fin s :=
…
```
def OAI.TwoPointCorrelations.jitterCode line 30
Source documentation
Finite version of a uniformly jittered residue, encoded in Q cells.
```
def jitterCode {s Q : ℕ} (r : Fin s) (j : Fin Q) : Fin Q :=
…
```
lemma OAI.TwoPointCorrelations.jitterCode_val line 33
lemma OAI.TwoPointCorrelations.jitterCode_sum line 37
Source documentation
Exact averaging identity for uniform residue and independent jitter.
```
lemma jitterCode_sum (s Q : ℕ) (F : Fin Q → ℝ) :
    (∑ r : Fin s, ∑ j : Fin Q, F (jitterCode r j)) =
      (s : ℝ) * ∑ k : Fin Q, F k := by
…
```
Mentions: OAI.TwoPointCorrelations.jitterCode
lemma OAI.TwoPointCorrelations.jitterCode_uniform line 50
Source documentation
The induced code kernel sends the uniform residue law to the uniform code law, exactly.
```
lemma jitterCode_uniform {s Q : ℕ} (hs : 0 < s) (hQ : 0 < Q) (k : Fin Q) :
    (∑ r : Fin s, (1 / (s : ℝ)) * finiteRandomKernel (@jitterCode s Q) r k) =
      1 / (Q : ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.finiteRandomKernel, OAI.TwoPointCorrelations.jitterCode
def OAI.TwoPointCorrelations.jitterDecode line 63
Source documentation
Decode the residue from the left endpoint of a code cell.
```
def jitterDecode {s Q : ℕ} (hs : 0 < s) (hQ : 0 < Q) (k : Fin Q) : Fin s :=
…
```
lemma OAI.TwoPointCorrelations.jitterDecode_code line 68
Source documentation
All jitter positions outside the first s positions decode correctly.
```
lemma jitterDecode_code {s Q : ℕ} (hs : 0 < s) (hQ : 0 < Q)
    (r : Fin s) (j : Fin Q) (hj : s ≤ j.val) :
    jitterDecode hs hQ (jitterCode r j) = r := by
…
```
Mentions: OAI.TwoPointCorrelations.jitterDecode, OAI.TwoPointCorrelations.jitterCode
theorem OAI.TwoPointCorrelations.jitterDecode_error line 84
Source documentation
Conditional decoding error for every fixed residue, independent of the law from which that residue was sampled.
```
theorem jitterDecode_error {s Q : ℕ} (hs : 0 < s) (hQ : 0 < Q) (r : Fin s) :
    (∑ j : Fin Q, if jitterDecode hs hQ (jitterCode r j) ≠ r then (1 : ℝ) else 0) /
        (Q : ℝ) ≤ (s : ℝ) / Q := by
…
```
Mentions: OAI.TwoPointCorrelations.jitterDecode, OAI.TwoPointCorrelations.jitterCode
def OAI.TwoPointCorrelations.binaryCellEquiv line 110
Source documentation
Any fixed bijective labeling of the 2^B cells by B bits suffices: the decoded equalities are represented by their truth tables.
```
noncomputable def binaryCellEquiv (B : ℕ) : Fin (2 ^ B) ≃ BooleanCube B :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
def OAI.TwoPointCorrelations.jitterBits line 113
def OAI.TwoPointCorrelations.decodeBits line 116
lemma OAI.TwoPointCorrelations.decode_jitterBits line 119
lemma OAI.TwoPointCorrelations.jitterBits_uniform line 124
Source documentation
Exact independent uniformity of the encoded bits under uniform residues.
```
lemma jitterBits_uniform {s B : ℕ} (hs : 0 < s) (x : BooleanCube B) :
    (∑ r : Fin s, (1 / (s : ℝ)) * finiteRandomKernel (@jitterBits s B) r x) =
      1 / (2 ^ B : ℕ) := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.finiteRandomKernel, OAI.TwoPointCorrelations.jitterBits