MRTFinalSampleScale.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The last ordinary prime band gives a separated-sample count strictly below the square-root scale. This is the count needed by the integer Gram kernel before the additional large-prime split.

lemma OAI.TwoPointCorrelations.mrt_final_sample_cost_pointwise line 13

theorem OAI.TwoPointCorrelations.mrt_final_prime_sample_cost line 120

Source documentation

Fixed eta=1/100 leaves a strict power saving below square-root sample size. The endpoint assumptions are only on the actual short prime bin.

theorem mrt_final_prime_sample_cost :
    ∀ᶠ L : ℝ in atTop, ∀ Y T α : ℝ, 1 < Y →
      200*Real.log L ≤ Real.log Y → Real.log Y ≤ Real.sqrt L →
      1 < T → T ≤ Real.exp L → 0 ≤ α → α ≤ 6/25 →
      mrtShortPrimeSampleCost Y (Real.exp (-α*Real.log Y)) T
        (mrtAmplificationOrder Y T) ≤ Real.exp ((99/200:ℝ)*L) := by
…

Mentions: OAI.TwoPointCorrelations.mrtShortPrimeSampleCost, OAI.TwoPointCorrelations.mrtAmplificationOrder

theorem OAI.TwoPointCorrelations.mrt_final_prime_large_samples line 147

Source documentation

Application to the literal finite prime polynomial.

theorem mrt_final_prime_large_samples :
    ∀ᶠ L : ℝ in atTop, ∀ Y T α : ℝ, 1 < Y →
      200*Real.log L ≤ Real.log Y → Real.log Y ≤ Real.sqrt L →
      1 < T → T ≤ Real.exp L → 0 ≤ α → α ≤ 6/25 →
      ∀ 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, Real.exp (-α*Real.log Y) ≤ ‖mrtExponentialPolynomial P
        (fun p => F p/(p:ℂ)) (fun p => -Real.log (p:ℝ)) t‖) →
      (S.card:ℝ) ≤ Real.exp ((99/200:ℝ)*L) := by
…

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