OAI/NumberTheory/JointDickman/Arithmetic/GrowingPrimeSamples.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.prime_block_reciprocal_mass line 10
2. theorem OAI.JointDickman.growing_prime_samples line 35

   Source documentation

   At threshold M^(-1/6), a block whose endpoints grow faster than a large logarithmic power has fewer than X^(5/12) separated large values.

   theorem growing_prime_samples : ∀ᶠ X : ℝ in atTop,
       ∀ M : ℕ, 2 ≤ M → 1 ≤ Real.log (M:ℝ) →
         (Real.log X)^100 ≤ (M:ℝ) → (M:ℝ) ≤ X^(1/100:ℝ) →
         ∀ P : Finset ℕ, (∀ p ∈ P, p.Prime ∧ (M:ℝ)/3 ≤ (p:ℝ) ∧ p ≤ M) →
         ∀ f : ℕ → ℂ, OneBounded f → ∀ V : ℝ, 0 < V → (M:ℝ)^(-1/6:ℝ) ≤ V →
         ∀ U : Finset ℝ, (∀ t ∈ U, |t| ≤ X) →
         (∀ x ∈ U, ∀ y ∈ U, x ≠ y → 1 ≤ |x-y|) →
         (∀ t ∈ U, V ≤ ‖mrtExponentialPolynomial P (fun p => f p/(p:ℂ))
           (fun p => -Real.log (p:ℝ)) t‖) → (U.card:ℝ) ≤ X^(5/12:ℝ) := by
   …