NearCofactorWindow.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Near-zero cancellation on the literal cofactor window

theorem OAI.JointDickman.near_zero_count_window line 12

Source documentation

Prefix cancellation on the near-zero frequency range passes to the actual reciprocal-count cofactor by finite partial summation.

theorem near_zero_count_window : ∃ C : ℝ, ∃ K : ℕ, 0 < C ∧ 2 ≤ K ∧
    ∀ (N : ℕ) (a : ℝ), 1 ≤ a → K ≤ ⌊(N:ℝ)/a⌋₊ →
    ∀ F : ℕ → ℂ, F 1 = 1 → Multiplicative F → OneBounded F →
    ∀ Q P : Finset ℕ, (∀ p ∈ Q, p.Prime) → (∀ p ∈ P, p.Prime) →
    (∀ p ∈ Q, (p:ℝ) ≤ Real.exp (Real.sqrt (Real.log (⌊(N:ℝ)/a⌋₊:ℝ)))) →
    squaredDistance F (mrtArchimedeanTwist 0) ⌊(2*N:ℝ)/a⌋₊ +
      (∑ p ∈ P, 1/(p:ℝ)) ≤ Real.log (Real.log (⌊(N:ℝ)/a⌋₊:ℝ))/8 →
    ∀ t : ℝ, |t| ≤ (Real.log (⌊(N:ℝ)/a⌋₊:ℝ))^((1:ℝ)/16) →
    ‖mrtCofactorPolynomial P (mrtMissingCoefficient F Q) N a t‖ ≤
      5*(2/(1+|t|)+C*(Real.log (⌊(N:ℝ)/a⌋₊:ℝ))^(-(1:ℝ)/16)) := by
…