OAI/NumberTheory/CubicMoment/Estimates/PrimeLogConvolution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual error in replacing a convolution of prime indicators by normalized von Mangoldt coefficients has sparse prime-power support.

  1. def OAI.CubicFirstMoment.primeLogConvolutionError line 14
  2. lemma OAI.CubicFirstMoment.primeLogConvolutionError_sum line 19
  3. lemma OAI.CubicFirstMoment.primeLogConvolutionError_support_of_norm_le line 28
  4. lemma OAI.CubicFirstMoment.primeLogConvolutionError_support line 60
  5. lemma OAI.CubicFirstMoment.primeLog_factor_norm_le line 73
  6. theorem OAI.CubicFirstMoment.primeLogConvolutionError_bound line 88

    Source documentation

    A divisor bound gives the genuine error coefficient a subpower amplitude.

    theorem primeLogConvolutionError_bound {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y : ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) → 1 ≤ Y →
      ∀ b ∈ orderedConvolutionSupport S, norm b ≤ Y →
      ‖primeLogConvolutionError S w b‖ ≤ C*Y^ε*(∏ i, M i) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeLogConvolutionError