DeterministicResidueSupply.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.eventually_high_residue_scale_window line 14
Source documentation
Uniform positivity and localization cutoff for every admissible real prime-product scale, not only the floor choice.
```
theorem eventually_high_residue_scale_window :
    ∀ᶠ S : ℝ in atTop, ∀ m : ℝ, S / (2 * Real.log S) ≤ m →
      0 ≤ m ∧ Real.exp (-m / 10000) ≤ 1 / 65536 := by
…
```
theorem OAI.Problem337.natural_product_phase_eq_differencing line 37
Source documentation
The two phase conventions agree exactly, including zero modulus where both divisions use their usual totalized field convention.
```
theorem natural_product_phase_eq_differencing (l C t u : ℕ) :
    Complex.exp (2 * Real.pi * Complex.I * (l * (C * t) : ℕ) / (u : ℂ)) =
      differencingPhase ((l : ℝ) * C * t / (u : ℝ)) := by
…
```
Mentions: OAI.Problem337.differencingPhase

theorem OAI.Problem337.deterministic_high_residue_distribution line 49

Source documentation

Unconditional deterministic high-level small-residue distribution. The only hypotheses concern the explicit scale, factor, size and distinctness of the list. Reciprocal cancellation, frequency moments, Markov selection and sharp localization are all discharged by the imported checked theorems.

theorem deterministic_high_residue_distribution (D : ℝ) (hD : 255 ≤ D) :
    ∀ᶠ S : ℝ in atTop, ∀ (m X : ℝ) (C : ℕ),
      S / (2 * Real.log S) ≤ m → m ≤ S / Real.log S →
      Real.exp S ≤ X → X ≤ Real.exp (D * S / 4) →
      Real.exp (D * S) ≤ (C : ℝ) → (C : ℝ) ≤ Real.exp (2 * D * S) →
      ∀ {ι : Type*} (T : Finset ι) (t : ι → ℕ),
        Set.InjOn t (T : Set ι) →
        Real.exp (Real.log 2 * m) ≤ (T.card : ℝ) →
        (∀ i ∈ T, (t i : ℝ) ≤ Real.exp (101 * S)) →
        ∃ E : Finset ℕ,
          E ⊆ Finset.Icc (⌊Real.exp (-m / 10000) * X⌋₊ + 1) ⌊X⌋₊ ∧
          (E.card : ℝ) ≤ X * Real.exp (-m / 1000) ∧
…

Mentions: OAI.Problem337.D