MRTExtraPrimeExtraction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Extraction through an additional prime band outside the original family. The original typical mask remains on the cofactor, and ordinary coprime multiplicativity suffices. The unsupported integers are retained as a separate, literal missing-band coefficient.

lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_outside_prime line 15
lemma OAI.TwoPointCorrelations.mrt_extra_prime_missing line 32
Source documentation
The exact missing-extra-band coefficient, before applying a sieve.
```
lemma mrt_extra_prime_missing (A : Finset ℕ) (C : ℕ → ℂ) (n : ℕ) :
    C n-mrtSupportedCoefficient A C n =
      if mrtPrimeAvoids A n then C n else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtSupportedCoefficient, OAI.TwoPointCorrelations.mrtPrimeAvoids

theorem OAI.TwoPointCorrelations.mrt_extra_prime_mean_square line 44

Source documentation

The additional-band factorization has the same uniform square and boundary error as the original bands, with no new factor for their count.

theorem mrt_extra_prime_mean_square {ι κ : Type*} [DecidableEq κ]
    (J : Finset ι) (P : ι → Finset ℕ)
    (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (A : Finset ℕ) (hA : ∀ p ∈ A, p.Prime)
    (hout : Disjoint A (J.biUnion P))
    (K : Finset κ) (bin : ℕ → κ) (hbin : ∀ p ∈ A, bin p ∈ K)
    (lower : κ → ℝ) {N : ℕ} (hN : 0 < N)
    {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ A, lower (bin p) ≤ p ∧ (p:ℝ) ≤ δ*lower (bin p))
    (F : ℕ → ℂ) (hF : Multiplicative F) (hFb : OneBounded F)
    {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T,
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded