BoolResidueDenominator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ResidueConstruction.pairedEntry_bool_reindex line 15
Source documentation
A Boolean-indexed sample block has exactly the same product as the Fin 2-indexed block used to construct the common denominator. In particular, this conversion never removes repeated sampled primes or repeated entries.
```
theorem pairedEntry_bool_reindex {m : ℕ}
    (q : (Fin m × Bool) → ℕ) (I : Fin m → Bool) :
    pairedEntry (fun j e => q (j, finTwoEquiv e))
      (fun j => finTwoEquiv.symm (I j)) = ∏ j, q (j, I j) := by
…
```
Mentions: OAI.Problem337.ResidueConstruction.pairedEntry

theorem OAI.Problem337.ResidueConstruction.construct_residue_denominator_bool line 24

Source documentation

The common denominator construction in the precise Boolean sample coordinates of the random Fourier theorem. The fixed deterministic list is still indexed by Fin m → Fin 2; the random lists retain their Boolean words.

theorem construct_residue_denominator_bool {m : ℕ} (p : Fin m → ℕ)
    (q : Fin 1000 → (Fin m × Bool) → ℕ)
    (hp : ∀ j, 0 < p j) (hq : ∀ i j e, 0 < q i (j, e)) {S : ℝ}
    (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S)
    (hlarge : 100 * Real.log S ≤ S)
    (hmLower : S - Real.log S ≤ (m : ℝ) * Real.log S)
    (hmUpper : (m : ℝ) * Real.log S ≤ S)
    (hpBounds : ∀ j, S ^ 100 ≤ (p j : ℝ) ∧ (p j : ℝ) ≤ S ^ 101)
    (hqBounds : ∀ i j e, (q i (j, e) : ℝ) ≤ S ^ 101) :
    ∃ M : ℕ, Real.exp S < (M : ℝ) ∧ (M : ℝ) ≤ Real.exp (204204 * S) ∧
      2 ^ ⌈100000 * Real.log S / Real.log 2⌉₊ ∣ M ∧
      (∀ I : Fin m → Fin 2, subsetEntry p I ∣ M ∧ 1 ≤ subsetEntry p I ∧
…

Mentions: OAI.Problem337.ResidueConstruction.subsetEntry

theorem OAI.Problem337.ResidueConstruction.scale_mul_log_bounds line 65
Source documentation
Both floor-scale inequalities needed by the common denominator, without an extra asymptotic assumption.
```
theorem scale_mul_log_bounds {S : ℝ} (hS : 0 < S) (hlog : 0 < Real.log S) :
    S - Real.log S ≤ (ResidueLevels.scale S : ℝ) * Real.log S ∧
      (ResidueLevels.scale S : ℝ) * Real.log S ≤ S := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale