EncodedCoefficients.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Low-order coefficients of the actual encoded interval law

A Walsh coefficient only uses the residue coordinates touched by its bits. All other independent jitters integrate out. The remaining observable is bounded by one, so CRT gives the product of its selected moduli divided by the interval length as an explicit coefficient bound.

lemma OAI.TwoPointCorrelations.finiteRandomKernel_expectation line 21
lemma OAI.TwoPointCorrelations.kernelTransport_expectation line 29
lemma OAI.TwoPointCorrelations.crtJitterBits_uniformAverage line 41
def OAI.TwoPointCorrelations.flattenBitBlocks line 57
Source documentation
Flatten bit blocks in the same order as the standard product equivalence Fin m × Fin B ≃ Fin (m*B).
```
def flattenBitBlocks (m B : ℕ) : (Fin m → BooleanCube B) ≃ BooleanCube (m * B) :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.flattenBitBlocks_apply line 61
def OAI.TwoPointCorrelations.bitSources line 65
Source documentation
Residue coordinates on which a given Walsh character depends.
```
def bitSources {m B : ℕ} (S : Finset (Fin (m * B))) : Finset (Fin m) :=
…
```
lemma OAI.TwoPointCorrelations.card_bitSources_le line 68
lemma OAI.TwoPointCorrelations.bitSource_mem line 71
def OAI.TwoPointCorrelations.extendBitBlocks line 75
Source documentation
Extend selected blocks by zero bits outside the selection.
```
def extendBitBlocks {m B : ℕ} (C : Finset (Fin m)) (z : C → BooleanCube B) : Fin m → BooleanCube B :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
def OAI.TwoPointCorrelations.selectedWalsh line 78
lemma OAI.TwoPointCorrelations.selectedWalsh_restrict line 82
lemma OAI.TwoPointCorrelations.abs_selectedWalsh line 90
def OAI.TwoPointCorrelations.integerBitSample line 95
Source documentation
The actual bits sampled from one uniformly chosen integer origin and independent finite jitters in every residue coordinate.
```
noncomputable def integerBitSample {m : ℕ} (s : Fin m → ℕ) [∀ i, NeZero (s i)]
    (B a : ℕ) {N : ℕ} (x : Fin N × (Fin m → Fin (2 ^ B))) : BooleanCube (m * B) :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
def OAI.TwoPointCorrelations.integerBitDensity line 99
lemma OAI.TwoPointCorrelations.integerBitDensity_nonneg line 103
lemma OAI.TwoPointCorrelations.integerBitDensity_mean line 107
def OAI.TwoPointCorrelations.selectedWalshMean line 114
Source documentation
The bounded observable on precisely the touched residue coordinates.
```
noncomputable def selectedWalshMean {m B : ℕ} (s : Fin m → ℕ)
    [∀ i, NeZero (s i)] (S : Finset (Fin (m * B)))
    (r : ∀ i : bitSources S, ZMod (s i)) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.bitSources
lemma OAI.TwoPointCorrelations.abs_selectedWalshMean_le_one line 120
lemma OAI.TwoPointCorrelations.crtJitterBits_restrict line 127
lemma OAI.TwoPointCorrelations.selectedWalshMean_eq_full line 132
lemma OAI.TwoPointCorrelations.selectedWalshMean_average_zero line 143
lemma OAI.TwoPointCorrelations.integerBitDensity_coefficient line 154
Source documentation
Each low-order coefficient is the actual selected-coordinate observable along the integer interval.
```
lemma integerBitDensity_coefficient {m B : ℕ} (s : Fin m → ℕ) [∀ i, NeZero (s i)]
    (a N : ℕ) (hN : 0 < N) (S : Finset (Fin (m * B))) :
    walshCoefficient (integerBitDensity s B a N) S =
      uniformAverage (fun j : Fin N =>
        selectedWalshMean s S (fun i : bitSources S => (a + j.val : ZMod (s i)))) := by
…
```
Mentions: OAI.TwoPointCorrelations.walshCoefficient, OAI.TwoPointCorrelations.integerBitDensity, OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.selectedWalshMean, OAI.TwoPointCorrelations.bitSources
theorem OAI.TwoPointCorrelations.integerBitDensity_coefficient_bound line 173
Source documentation
The Fourier error for a set of bits is bounded by the product of the moduli of the residue coordinates touched by those bits, divided by length.
```
theorem integerBitDensity_coefficient_bound {m B : ℕ} (s : Fin m → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (a N : ℕ) (hN : 0 < N) (S : Finset (Fin (m * B))) (hS : S.Nonempty) :
    |walshCoefficient (integerBitDensity s B a N) S| ≤
      (∏ i : bitSources S, s i : ℕ) / (N : ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.walshCoefficient, OAI.TwoPointCorrelations.integerBitDensity, OAI.TwoPointCorrelations.bitSources
lemma OAI.TwoPointCorrelations.selected_modulus_product_le line 194
lemma OAI.TwoPointCorrelations.integerBitDensity_low_coefficients line 205

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.encoded_interval_comparison line 219

Source documentation

Finite-parameter encoded residue comparison derived from the published Braverman input, with all Fourier errors discharged by the actual interval sampling law. Only the final numerical error budget is left to choose.

theorem BravermanDepth22Input.encoded_interval_comparison (hBraverman : BravermanDepth22Input) :
    ∃ K C : ℕ, 0 < K ∧ 0 < C ∧ ∀ (m B : ℕ), 0 < m * B →
      ∀ (s : Fin m → ℕ) [∀ i, NeZero (s i)],
      Pairwise (fun i j => (s i).Coprime (s j)) →
      ∀ (c : AC0Circuit (m * B)), c.depth ≤ 22 →
      ∀ ε : ℝ, 0 < ε → ε ≤ 1 / 2 → ∀ t : ℕ,
        (K : ℝ) * (Real.log ((c.size : ℝ) / ε)) ^ C ≤ (t : ℝ) →
        ∀ (a N : ℕ), 0 < N → ∀ M A : ℝ, 1 ≤ M → (∀ i, (s i : ℝ) ≤ M) →
          (M ^ t / (N : ℝ)) * ((t + 1 : ℕ) : ℝ) * ((m * B : ℕ) : ℝ) ^ t ≤ A →
          |uniformAverage (fun x : Fin N × (Fin m → Fin (2 ^ B)) =>
              c.indicator (integerBitSample s B a x)) - cubeAverage c.indicator| ≤
            3 * A / 2 + ε := by
…

Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.integerBitSample, OAI.TwoPointCorrelations.cubeAverage