FiniteLawParameters.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit large-scale choices for the finite residue comparison.

lemma OAI.TwoPointCorrelations.eventually_const_mul_pow_le line 13
Source documentation
Fixed coefficients are absorbed by increasing a positive integer power.
```
lemma eventually_const_mul_pow_le (p q : ℕ) (hpq : p < q) (c : ℝ) :
    ∀ᶠ L : ℝ in atTop, c * L ^ p ≤ L ^ q := by
…
```
lemma OAI.TwoPointCorrelations.ceil_pow_bounds line 21

lemma OAI.TwoPointCorrelations.eventually_encoded_size_bound line 27

Source documentation

Truth-table substitution fits the manuscript's encoded size bound.

lemma eventually_encoded_size_bound :
    ∀ᶠ L : ℝ in atTop, ∀ B : ℕ, B = ⌈L ^ 15⌉₊ →
      ∀ S : ℝ, S ≤ Real.exp (L ^ 6) →
      (1 + (2 : ℝ) ^ B * (1 + B)) * S ≤ Real.exp (L ^ 17) := by
…

lemma OAI.TwoPointCorrelations.eventually_bit_count_bound line 67

Source documentation

The number of bits is small even after adding the fixed-modulus block.

lemma eventually_bit_count_bound :
    ∀ᶠ L : ℝ in atTop, ∀ m B : ℕ, (m : ℝ) ≤ Real.exp L + 1 → B = ⌈L ^ 15⌉₊ →
      ((m * B : ℕ) : ℝ) ≤ Real.exp (2 * L) := by
…

lemma OAI.TwoPointCorrelations.eventually_braverman_budget line 90

Source documentation

Polynomially many independence coordinates suffice for Braverman's logarithmic requirement at encoded size exp (L^17).

lemma eventually_braverman_budget (K C : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ S : ℝ, 1 ≤ S → S ≤ Real.exp (L ^ 17) →
      (K : ℝ) * (Real.log (S / Real.exp (-(L ^ 11)))) ^ C ≤
        (⌈L ^ (17 * C + 1)⌉₊ : ℝ) := by
…

lemma OAI.TwoPointCorrelations.eventually_fourier_budget line 118

Source documentation

The actual low-order Fourier mass is exponentially small once the interval exponent exceeds the independence exponent.

lemma eventually_fourier_budget (T A : ℕ) (hT : 10 ≤ T) (hA : T + 1 < A) :
    ∀ᶠ L : ℝ in atTop, ∀ t n N : ℕ, t = ⌈L ^ T⌉₊ →
      (n : ℝ) ≤ Real.exp (2 * L) → Real.exp (L ^ A / 2) ≤ (N : ℝ) →
      ((Real.exp L) ^ t / (N : ℝ)) * ((t + 1 : ℕ) : ℝ) * (n : ℝ) ^ t ≤
        Real.exp (-(L ^ 11)) := by
…

lemma OAI.TwoPointCorrelations.eventually_total_comparison_error line 158

Source documentation

Both decoder errors and the corrected-law errors fit inside the final exp (-L^10) budget.

lemma eventually_total_comparison_error :
    ∀ᶠ L : ℝ in atTop, ∀ B : ℕ, B = ⌈L ^ 15⌉₊ → ∀ D : ℝ,
      D ≤ Real.exp (3 * L) →
      2 * D / (2 : ℝ) ^ B + 3 * Real.exp (-(L ^ 11)) / 2 +
        Real.exp (-(L ^ 11)) ≤ Real.exp (-(L ^ 10)) := by
…

lemma OAI.TwoPointCorrelations.eventually_scalar_error line 207
Source documentation
The coefficient mass allowed in scalar expansions consumes only one power in the exponent of the finite-law error.
```
lemma eventually_scalar_error (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 5) * Real.exp (-(L ^ 10)) ≤ Real.exp (-(L ^ 9)) := by
…
```