CRTComparison.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Finite CRT marginals and contraction under independent randomization

A selected finite set of pairwise coprime residue coordinates has the law of one residue modulo their product. The exact interval count from ResidueCounts gives total variation at most D / (2N). Applying any finite stochastic kernel preserves this bound; in particular one may add independent finite randomness and project to any selected encoded bits. These are the finite arithmetic and data-processing steps in q:crt-bits.

def OAI.TwoPointCorrelations.finiteTotalVariation line 23
Source documentation
Total variation between two finite real mass functions.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:23 (same declaration text).
```
noncomputable def finiteTotalVariation {α : Type*} [Fintype α] (f g : α → ℝ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.kernelTransport line 27
Source documentation
Application of a finite transition kernel.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:27 (same declaration text).
```
noncomputable def kernelTransport {α β : Type*} [Fintype α]
    (K : α → β → ℝ) (f : α → ℝ) (y : β) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.kernelTransport_nonneg line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.kernelTransport_sum line 36
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:36 (same declaration text).
theorem OAI.TwoPointCorrelations.finiteTotalVariation_kernel line 45
Source documentation
Adding independent randomness and then forgetting information cannot increase total variation.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:45 (same declaration text).
```
theorem finiteTotalVariation_kernel {α β : Type*} [Fintype α] [Fintype β]
    (K : α → β → ℝ) (f g : α → ℝ) (hK : ∀ x y, 0 ≤ K x y)
    (hKsum : ∀ x, ∑ y, K x y = 1) :
    finiteTotalVariation (kernelTransport K f) (kernelTransport K g) ≤
      finiteTotalVariation f g := by
…
```
Mentions: OAI.TwoPointCorrelations.finiteTotalVariation, OAI.TwoPointCorrelations.kernelTransport
lemma OAI.TwoPointCorrelations.finite_observable_difference line 68
Source documentation
A bounded observable has expectation difference at most twice TV.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:68 (same declaration text).
```
lemma finite_observable_difference {α : Type*} [Fintype α]
    (f g u : α → ℝ) (hu : ∀ x, |u x| ≤ 1) :
    |(∑ x, f x * u x) - ∑ x, g x * u x| ≤ 2 * finiteTotalVariation f g := by
…
```
Mentions: OAI.TwoPointCorrelations.finiteTotalVariation
def OAI.TwoPointCorrelations.finiteRandomKernel line 87
Source documentation
A deterministic map with independent uniform finite auxiliary randomness.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:87 (same declaration text).
```
noncomputable def finiteRandomKernel {α β J : Type*} [DecidableEq β] [Fintype J]
    (F : α → J → β) (x : α) (y : β) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.finiteRandomKernel_nonneg line 91
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:91 (same declaration text).
lemma OAI.TwoPointCorrelations.finiteRandomKernel_sum line 96
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:96 (same declaration text).
instance OAI.TwoPointCorrelations.modulusProduct_neZero line 103
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:103 (same declaration text).

def OAI.TwoPointCorrelations.crtJointProbability line 108

Source documentation

The actual joint residue law of an interval under the CRT equivalence.

Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:108 (same declaration text).

noncomputable def crtJointProbability {ι : Type*} [Fintype ι] [DecidableEq ι] (s : ι → ℕ)
    [∀ i, NeZero (s i)] (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (r : ∀ i, ZMod (s i)) : ℝ :=
…

def OAI.TwoPointCorrelations.crtUniform line 114
Source documentation
Uniform independent residue coordinates.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:114 (same declaration text).
```
noncomputable def crtUniform {ι : Type*} [Fintype ι] [DecidableEq ι] (s : ι → ℕ)
    (_r : ∀ i, ZMod (s i)) : ℝ := 1 / (∏ i, s i : ℕ)
```
lemma OAI.TwoPointCorrelations.crtUniform_product line 117
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:117 (same declaration text).

lemma OAI.TwoPointCorrelations.crtJointProbability_eq_count line 122

Source documentation

This CRT-transported mass is the actual empirical joint residue law.

Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:122 (same declaration text).

lemma crtJointProbability_eq_count {ι : Type*} [Fintype ι] [DecidableEq ι] (s : ι → ℕ)
    [∀ i, NeZero (s i)] (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (r : ∀ i, ZMod (s i)) :
    crtJointProbability s hcop A N r =
      (∑ j ∈ Finset.range N,
        if ZMod.prodEquivPi s hcop (A + (j : ZMod (∏ i, s i))) = r
          then (1 : ℝ) else 0) / N := by
…

Mentions: OAI.TwoPointCorrelations.crtJointProbability

lemma OAI.TwoPointCorrelations.crt_coordinates_add_nat line 140

Source documentation

The CRT equivalence is the expected coordinatewise residue map.

Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:140 (same declaration text).

lemma crt_coordinates_add_nat {ι : Type*} [Fintype ι] [DecidableEq ι] (s : ι → ℕ)
    [∀ i, NeZero (s i)] (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (j : ℕ) (i : ι) :
    ZMod.prodEquivPi s hcop (A + (j : ZMod (∏ i, s i))) i =
      ZMod.castHom (Finset.dvd_prod_of_mem s (Finset.mem_univ i)) (ZMod (s i)) A +
        (j : ZMod (s i)) := by
…

lemma OAI.TwoPointCorrelations.crtJointProbability_nonneg line 148
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:148 (same declaration text).
lemma OAI.TwoPointCorrelations.crtJointProbability_sum line 155
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:155 (same declaration text).
lemma OAI.TwoPointCorrelations.crtJointProbability_totalVariation line 165
Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:165 (same declaration text).

theorem OAI.TwoPointCorrelations.crt_kernel_totalVariation line 177

Source documentation

Selected CRT coordinates followed by any finite random encoding or projection satisfy the interval discrepancy bound.

Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:177 (same declaration text).

theorem crt_kernel_totalVariation {ι β : Type*} [Fintype ι] [DecidableEq ι] [Fintype β]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (hN : 0 < N)
    (K : (∀ i, ZMod (s i)) → β → ℝ)
    (hK : ∀ r y, 0 ≤ K r y) (hKsum : ∀ r, ∑ y, K r y = 1) :
    finiteTotalVariation (kernelTransport K (crtJointProbability s hcop A N))
      (kernelTransport K (crtUniform s)) ≤ (∏ i, s i : ℕ) / (2 * (N : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.finiteTotalVariation, OAI.TwoPointCorrelations.kernelTransport, OAI.TwoPointCorrelations.crtJointProbability, OAI.TwoPointCorrelations.crtUniform

theorem OAI.TwoPointCorrelations.crt_random_projection_totalVariation line 191

Source documentation

Independent finite auxiliary variables and a projection are a special case, so in particular selecting encoded bit marginals cannot increase TV.

Also declared: OAI/NumberTheory/TwoPointCorrelations/CRTComparison.lean:191 (same declaration text).

theorem crt_random_projection_totalVariation {ι β J : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype β] [DecidableEq β] [Fintype J] [Nonempty J]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i)) (N : ℕ) (hN : 0 < N)
    (F : (∀ i, ZMod (s i)) → J → β) :
    finiteTotalVariation
      (kernelTransport (finiteRandomKernel F) (crtJointProbability s hcop A N))
      (kernelTransport (finiteRandomKernel F) (crtUniform s)) ≤
        (∏ i, s i : ℕ) / (2 * (N : ℝ)) :=
…

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