CharacterTruncation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Inserting the published character bound below the square-root cutoff

theorem OAI.JointDickman.smallCharacterConvolution_bound line 11

theorem OAI.JointDickman.roughCharacterSum_truncated line 40

Source documentation

Uniformity in the modulus is inherited from the published input. The large-divisor remainder is the actual, already bounded convolution tail.

theorem roughCharacterSum_truncated
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) {C D : ℝ} (hC : 0 < C) (hD : 0 ≤ D) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (E : Finset ℕ) (Y : ℝ) (V : ℕ),
      9 ≤ Y → (V : ℝ) ^ 2 ≤ Y → ∀ (q : ℕ) [NeZero q],
      (q : ℝ) ≤ (Real.log Y / 2) ^ C → ∀ χ : DirichletCharacter ℂ q, χ ≠ 1 →
      ‖roughCharacterSum χ E z Y‖ ≤
        K * Y * (Real.log Y / 2) ^ (-D) *
          (∑ v ∈ Ioc 0 V, |smoothCorrection E z v| / (v : ℝ)) +
        ‖characterConvolutionTail χ E z ⌊Y⌋₊ V‖ := by
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.roughCharacterSum, OAI.JointDickman.smoothCorrection, OAI.JointDickman.characterConvolutionTail