MRTMissingBandSieve.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite missing-band sieve in MRT, with its full Bonferroni and interval-boundary errors. CRT, not an independence assumption on integers, supplies every intersection estimate.

theorem OAI.TwoPointCorrelations.mrt_prime_avoidance_probability line 16
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMissingBandSieve.lean:16 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_missing_band_probability line 45

Source documentation

Mertens supplies the main term log P/log Q; both finite-sieve errors remain explicit for choosing the typical-factorization parameters.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMissingBandSieve.lean:45 (same declaration text).

theorem mrt_missing_band_probability : ∃ C : ℝ, 0 < C ∧
    ∀ (P Q : ℝ), 2 ≤ P → P ≤ Q → ∀ (A N : ℕ) [NeZero N] (r : ℕ),
    (uniformFiniteLaw (Fin N)).probability
      (fun j => mrtPrimeAvoids (mrtPrimeBand P Q) (A + j.val)) ≤
      C * Real.log P / Real.log Q +
        Real.exp (2 * ∑ p ∈ mrtPrimeBand P Q, 1 / (p : ℝ)) / (2 : ℝ) ^ (2 * r + 1) +
        1 / (N : ℝ) * (2 * r + 1 : ℕ) *
          (((mrtPrimeBand P Q).card : ℝ) * Q + 1) ^ (2 * r) := by
…

Mentions: OAI.TwoPointCorrelations.uniformFiniteLaw, OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.mrtPrimeBand

theorem OAI.TwoPointCorrelations.mrtTypical_missing_union line 64
Source documentation
Failure of typical factorization is a union of the literal missing-band events, so the numerical single-band bounds add without any independence.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMissingBandSieve.lean:64 (same declaration text).
```
theorem mrtTypical_missing_union {ι α : Type*} [Fintype ι] [Fintype α]
    (P : ι → Finset ℕ) (μ : FiniteLaw α) (n : α → ℕ) :
    μ.probability (fun x => ¬mrtTypical univ P (n x)) ≤
      ∑ i, μ.probability (fun x => mrtPrimeAvoids (P i) (n x)) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.mrtPrimeAvoids