OAI/NumberTheory/JointDickman/Analysis/MellinProductSamples.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.mellin_product_sample_split line 14

   Source documentation

   Split the finite product energy at the prime-polynomial threshold. Only the large-prime class needs the pointwise cofactor bound.

   lemma mellin_product_sample_split (S : Finset ℝ) (Q R : ℝ → ℂ)
       {τ b : ℝ} (_hτ : 0 ≤ τ)
       (hR : ∀ t ∈ S, τ < ‖Q t‖ → ‖R t‖ ≤ b) :
       (∑ t ∈ S, ‖Q t*R t‖^2) ≤
         τ^2*(∑ t ∈ S, ‖R t‖^2)+
           b^2*(∑ t ∈ S.filter (fun t => τ < ‖Q t‖), ‖Q t‖^2) := by
   …

2. theorem OAI.JointDickman.ramare_product_sparse_samples line 49

   Source documentation

   Auxiliary-prime sampling in terms of sample counts and cofactor values.

   theorem ramare_product_sparse_samples (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) →
         ∀ (S : Finset ℝ) (T τ b : ℝ), 0 ≤ T → 0 ≤ τ →
         (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|) →
         (∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ T) → T ≤ a^B →
         let Qf := mrtExponentialPolynomial Q (fun p => f p/(p:ℂ))
   …