SparseIntegerMellin.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sparse sampling of the actual integer cofactor polynomial

theorem OAI.JointDickman.sparse_integer_mellin_sampling line 11

Source documentation

Finite duality for sharp integer intervals, with the square-root frequency error charged only once per sampled point.

theorem sparse_integer_mellin_sampling {U : ℝ} (hU : 1 ≤ U) (L R : ℕ)
    (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U)
    (S : Finset ℝ) (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
    {T : ℝ} (hT : 0 ≤ T) (hdiam : ∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ T)
    (a : ℕ → ℂ) :
    (∑ t ∈ S, ‖mrtExponentialPolynomial (Icc L R) a
      (fun n => -Real.log (n:ℝ)) t‖^2) ≤
      16000*(2*U*(1+Real.log (T+1))+(S.card:ℝ)*Real.sqrt T)*
        ∑ n ∈ Icc L R, ‖a n‖^2 := by
…

lemma OAI.JointDickman.reciprocal_cofactor_mass line 26

theorem OAI.JointDickman.sparse_reciprocal_cofactor_sampling line 52

Source documentation

The normalized cofactor estimate required in the small-prime class of the exceptional-frequency decomposition. Coefficients may already include finite-prime masks and the reciprocal prime-count weight.

theorem sparse_reciprocal_cofactor_sampling {U : ℝ} (hU : 1 ≤ U) (L R : ℕ)
    (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U)
    (S : Finset ℝ) (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
    {T : ℝ} (hT : 0 ≤ T) (hdiam : ∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ T)
    (a : ℕ → ℂ) (ha : ∀ n ∈ Icc L R, ‖a n‖ ≤ 1/(n:ℝ)) :
    (∑ t ∈ S, ‖mrtExponentialPolynomial (Icc L R) a
      (fun n => -Real.log (n:ℝ)) t‖^2) ≤
      48000*(2*(1+Real.log (T+1))+(S.card:ℝ)*Real.sqrt T/U) := by
…