BitMarginals.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Joint finite jitter and independent uniform bit blocks

The permutation underlying one-coordinate jitter acts independently in every coordinate. This proves exact joint uniformity before selecting any bits; together with CRT contraction it gives finite quantitative marginal comparison, including arbitrary fixed non-squarefree moduli.

def OAI.TwoPointCorrelations.coordinatePairEquiv line 20

Source documentation

Split a family of pairs into a pair of families.

def coordinatePairEquiv {ι : Type*} (α β : ι → Type*) :
    (∀ i, α i × β i) ≃ (∀ i, α i) × (∀ i, β i) where
…

def OAI.TwoPointCorrelations.jointJitterPermutation line 27
def OAI.TwoPointCorrelations.jointJitterCode line 33
lemma OAI.TwoPointCorrelations.jointJitterCode_sum line 37

lemma OAI.TwoPointCorrelations.jointJitterCode_uniform line 51

Source documentation

Exact uniformity of all code coordinates under uniform residues.

lemma jointJitterCode_uniform {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)] {Q : ℕ} (hQ : 0 < Q) (k : ι → Fin Q) :
    (∑ r : ∀ i, Fin (s i), (1 / (∏ i, s i : ℕ)) *
      finiteRandomKernel (@jointJitterCode ι s Q) r k) =
        1 / (Fintype.card (ι → Fin Q) : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.finiteRandomKernel, OAI.TwoPointCorrelations.jointJitterCode

def OAI.TwoPointCorrelations.crtJitterCode line 66

Source documentation

Evaluate joint finite jitter directly on CRT residue coordinates.

noncomputable def crtJitterCode {ι : Type*} (s : ι → ℕ) [∀ i, NeZero (s i)] {Q : ℕ}
    (r : ∀ i, ZMod (s i)) (j : ι → Fin Q) : ι → Fin Q :=
…

lemma OAI.TwoPointCorrelations.crtJitterCode_uniform line 70

theorem OAI.TwoPointCorrelations.crtJitterCode_totalVariation line 90

Source documentation

A selected family of residue coordinates, encoded jointly, differs from independent uniform code coordinates by at most D/(2N) in total variation.

theorem crtJitterCode_totalVariation {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (hN : 0 < N) {Q : ℕ} (hQ : 0 < Q) :
    finiteTotalVariation
      (kernelTransport (finiteRandomKernel (@crtJitterCode ι s _ Q))
        (crtJointProbability s hcop A N))
      (fun _ => 1 / (Fintype.card (ι → Fin Q) : ℝ)) ≤
        (∏ i, s i : ℕ) / (2 * (N : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.finiteTotalVariation, OAI.TwoPointCorrelations.kernelTransport, OAI.TwoPointCorrelations.finiteRandomKernel, OAI.TwoPointCorrelations.crtJitterCode, OAI.TwoPointCorrelations.crtJointProbability

def OAI.TwoPointCorrelations.jointBitEquiv line 108
Source documentation
Coordinatewise conversion of uniform integer cells into bit blocks.
```
noncomputable def jointBitEquiv (ι : Type*) (B : ℕ) :
    (ι → Fin (2 ^ B)) ≃ (ι → BooleanCube B) :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
def OAI.TwoPointCorrelations.crtJitterBits line 112
lemma OAI.TwoPointCorrelations.crtJitterBits_uniform line 116

theorem OAI.TwoPointCorrelations.crtJitterBits_totalVariation line 141

Source documentation

Exact joint uniform bit law and the interval comparison error, before projecting to any subset of these bits.

theorem crtJitterBits_totalVariation {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (hN : 0 < N) (B : ℕ) :
    finiteTotalVariation
      (kernelTransport (finiteRandomKernel (crtJitterBits s B)) (crtJointProbability s hcop A N))
      (fun _ => 1 / (Fintype.card (ι → BooleanCube B) : ℝ)) ≤
        (∏ i, s i : ℕ) / (2 * (N : ℝ)) := by
…