SparseCofactorSampling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse sampling for the reciprocal-count cofactor used by Ramaré

theorem OAI.JointDickman.sparse_ramare_cofactor_sampling line 12

Source documentation

The sparse integer estimate applies to the literal cofactor, including all bounded coefficient masks and the reciprocal prime-divisor count.

theorem sparse_ramare_cofactor_sampling (P : Finset ℕ) (F : ℕ → ℂ)
    (hF : OneBounded F) (N : ℕ) {a : ℝ} (ha : 1 ≤ a)
    (hx : 2 ≤ (N:ℝ)/a) (S : Finset ℝ)
    (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
    {T : ℝ} (hT : 0 ≤ T) (hdiam : ∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ T) :
    (∑ t ∈ S, ‖mrtCofactorPolynomial P F N a t‖^2) ≤
      48000*(2*(1+Real.log (T+1))+(S.card:ℝ)*Real.sqrt T*a/N) := by
…