MRTExtraSampleScale.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The large-value sample count for the additional prime interval. The lower-endpoint complement 1/80 is deliberately smaller than the published proof's optimized choice; it preserves the exact MRT input rates.

lemma OAI.TwoPointCorrelations.mrt_extra_sample_cost_pointwise line 14
theorem OAI.TwoPointCorrelations.mrt_extra_prime_sample_cost line 117
Source documentation
Uniform large-extra-prime sample cost. The remaining Mangoldt kernel will have much stronger decay than this subexponential cardinality.
```
theorem mrt_extra_prime_sample_cost :
    ∀ᶠ L : ℝ in atTop, ∀ Y T : ℝ, 1 < Y →
      L^(79/(80:ℝ)) ≤ Real.log Y → Real.log Y ≤ L →
      1 < T → T ≤ Real.exp L →
      mrtShortPrimeSampleCost Y (L^(-100:ℝ)) T (mrtAmplificationOrder Y T) ≤
        Real.exp (L^(3/(100:ℝ))) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtShortPrimeSampleCost, OAI.TwoPointCorrelations.mrtAmplificationOrder

theorem OAI.TwoPointCorrelations.mrt_extra_prime_large_samples line 142

Source documentation

The preceding optimized cost bounds the actual separated large-value samples of every additional short prime interval.

theorem mrt_extra_prime_large_samples :
    ∀ᶠ L : ℝ in atTop, ∀ Y T : ℝ, 1 < Y →
      L^(79/(80:ℝ)) ≤ Real.log Y → Real.log Y ≤ L →
      1 < T → T ≤ Real.exp L →
      ∀ P : Finset ℕ, (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, Y ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*Y) →
      ∀ F : ℕ → ℂ, OneBounded F → ∀ S : Finset ℝ,
      (∀ t ∈ S, |t| ≤ T) →
      (∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) →
      (∀ t ∈ S, L^(-100:ℝ) ≤ ‖mrtExponentialPolynomial P
        (fun p => F p/(p:ℂ)) (fun p => -Real.log (p:ℝ)) t‖) →
      (S.card:ℝ) ≤ Real.exp (L^(3/(100:ℝ))) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtExponentialPolynomial