OAI/NumberTheory/JointDickman/Amplification/RamareProductIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.ramare_product_sparse_integral line 13

   Source documentation

   The two sample-cardinality premises concern literal finite subsets of E. The prime and cofactor sampling estimates themselves are proved.

   theorem ramare_product_sparse_integral (B : ℝ) (hB : 1 ≤ B) :
       ∃ C γ : ℝ, 0 < C ∧ 0 < γ ∧
         ∀ᶠ a : ℝ in atTop, ∀ (N : ℕ) (P Q : Finset ℕ) (F f : ℕ → ℂ),
         1 ≤ a → 2 ≤ (N:ℝ)/a → OneBounded F → OneBounded f →
         (∀ p ∈ Q, p.Prime ∧ a ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*a) →
         ∀ (E : Set ℝ) (T τ b K : ℝ), MeasurableSet E → 0 ≤ T → 0 ≤ τ →
         E ⊆ Set.Ioc (-T) T → 2*T ≤ a^B →
         let Qf := mrtExponentialPolynomial Q (fun p => f p/(p:ℂ))
   …