RandomResidueRealization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RandomProducts.sampledRemainder line 14
Source documentation
The least nonnegative remainder used by numerator descent, for an actual labelled prime sample and an actual Boolean choice.
```
def sampledRemainder {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u : ℕ) (I : Fin m → Bool) : ℕ :=
…
```

theorem OAI.Problem337.RandomProducts.sampled_remainder_count_of_fourier line 20

Source documentation

The exact, normalized random Fourier bound gives the half-mass small-remainder bound. Indexed repeated products are retained.

theorem sampled_remainder_count_of_fourier {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u : ℕ) (hu : 0 < u) (w : ℝ)
    (hw : 10000 * Real.log 65536 ≤ w)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (4 * w / 10000)⌋₊ →
      ‖sampledMean p u l‖ ≤ Real.exp (-3 * w / 10000)) :
    (Real.exp (-w / 10000) / 2) * (2 : ℝ) ^ m ≤
      ((Finset.univ.filter (fun I : Fin m → Bool =>
        (sampledRemainder p u I : ℝ) < Real.exp (-w / 10000) * u)).card : ℝ) := by
…

Mentions: OAI.Problem337.RandomProducts.sampledMean, OAI.Problem337.RandomProducts.sampledRemainder

theorem OAI.Problem337.RandomProducts.exists_sampled_terminal_remainder line 56

Source documentation

Every Fourier-good terminal modulus has an actual Boolean product with remainder smaller than the required power of that modulus.

theorem exists_sampled_terminal_remainder {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u : ℕ) (hu : 0 < u)
    (hw : 10000 * Real.log 65536 ≤ Real.log (u : ℝ))
    (hfourier : ∀ l : ℕ, 1 ≤ l →
      l ≤ ⌊Real.exp (4 * Real.log (u : ℝ) / 10000)⌋₊ →
      ‖sampledMean p u l‖ ≤ Real.exp (-3 * Real.log (u : ℝ) / 10000)) :
    ∃ I : Fin m → Bool,
      (sampledRemainder p u I : ℝ) < (u : ℝ) ^ (9999 / 10000 : ℝ) := by
…

Mentions: OAI.Problem337.RandomProducts.sampledMean, OAI.Problem337.RandomProducts.sampledRemainder

def OAI.Problem337.RandomProducts.residueFrequencies line 84
Source documentation
The finite Fourier frequency window used at every scale.
```
def residueFrequencies (w : ℝ) : Finset ℕ :=
…
```

theorem OAI.Problem337.RandomProducts.exists_common_sampled_residue_realization line 90

Source documentation

A common choice of actual prime samples supplies the middle-level small-remainder counts and covers every prescribed terminal numerator. All hypotheses are explicit finite size/range conditions.

theorem exists_common_sampled_residue_realization :
    ∃ N : ℕ, ∀ (S : ℝ) (P : Finset ℕ) (J : Type)
      (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ)
      (terminal : Finset ℕ),
      3 ≤ S →
      (∀ p ∈ P, Nat.Prime p) →
      (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
      S ^ 99 ≤ (P.card : ℝ) →
      500000 ≤ (blockLength S : ℝ) →
      10000 * Real.log 65536 ≤ (blockLength S : ℝ) →
      (tests.card : ℝ) ≤ (blockLength S : ℝ) →
      (∀ j ∈ tests, 0 < X j) →
…

Mentions: OAI.Problem337.RandomProducts.blockLength

theorem OAI.Problem337.RandomProducts.sampledRemainder_eq_real_ceil line 191
Source documentation
Rational and real ceiling remainder formulas agree exactly.
```
theorem sampledRemainder_eq_real_ceil {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u : ℕ) (hu : 0 < u) (I : Fin m → Bool) :
    sampledRemainder p u I =
      u * ⌈(sampledProduct p I : ℝ) / u⌉₊ - sampledProduct p I := by
…
```
Mentions: OAI.Problem337.RandomProducts.sampledRemainder, OAI.Problem337.RandomProducts.sampledProduct
theorem OAI.Problem337.RandomProducts.sampledRemainder_lt_iff_fract line 202
Source documentation
A sampled rational-ceiling remainder has exactly the same normalized fractional-part interpretation as the real-ceiling construction.
```
theorem sampledRemainder_lt_iff_fract {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u : ℕ) (hu : 0 < u)
    (I : Fin m → Bool) (δ : ℝ) :
    (sampledRemainder p u I : ℝ) < δ * u ↔
      Int.fract (-(sampledProduct p I : ℝ) / u) < δ := by
…
```
Mentions: OAI.Problem337.RandomProducts.sampledRemainder, OAI.Problem337.RandomProducts.sampledProduct

theorem OAI.Problem337.RandomProducts.exists_common_sampled_residue_realization_strict line 215

Source documentation

A common choice of actual prime samples supplies the middle-level small-remainder counts and covers every prescribed terminal numerator. All hypotheses are explicit finite size/range conditions.

theorem exists_common_sampled_residue_realization_strict :
    ∃ N : ℕ, ∀ (S : ℝ) (P : Finset ℕ) (J : Type)
      (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ)
      (terminal : Finset ℕ),
      3 ≤ S →
      (∀ p ∈ P, Nat.Prime p) →
      (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
      S ^ 99 ≤ (P.card : ℝ) →
      500000 ≤ (blockLength S : ℝ) →
      10000 * Real.log 65536 ≤ (blockLength S : ℝ) →
      (tests.card : ℝ) ≤ (blockLength S : ℝ) →
      (∀ j ∈ tests, 0 < X j) →
…

Mentions: OAI.Problem337.RandomProducts.blockLength