ElevenTwelfths.ZetaBound

ElevenTwelfths
ZetaBound

import ElevenTwelfths.ZetaFamily
import ElevenTwelfths.Unconditional

The amplified Möbius estimate in the guide's notation

The all-element sixth-power average produces the totient density, rather than the unweighted sum. We expose that coefficient and specialize the existing unconditional estimate to zeta; no Dirichlet character parameter appears in the public statement.

namespace ElevenTwelfths.Zetanoncomputable sectionopen scoped BigOperators Classical Topologyopen Filter Asymptoticsopen OAI OAI.ActualEisensteinCubicopen OAI.SixthPowerAverageopen OAI.ConcretePrimeRowBridgeopen OAI.ShortDraftHeckeBridge

The density of amplifier elements coprime to n.

abbrev density (n : Ideal 𝒪) : ℂ :=
  ∏ P ∈ OAI.IdealMobiusDivisorSum.primeSupport n,
    (1 - (1 : ℂ) / (Ideal.absNorm P : ℂ))

The weighted Möbius sum actually produced by the smooth amplifier.

def densityM (W : SmoothDyadicWeight ℂ) (X : ℝ) : ℂ :=
  ∑' n : Ideal 𝒪, if ∀ P ∈ excludedPrimes, ¬ P ∣ n then
    (UniqueFactorizationMonoid.moebius n : ℂ) * density n *
      W ((Ideal.absNorm n : ℝ) / X) else 0

theorem densityM_eq_outsideWeight (W : SmoothDyadicWeight ℂ) (X : ℝ) :
    densityM W X = ∑' n : Ideal 𝒪,
      outsideWeight (1 : DirichletCharacter ℂ 1) excludedPrimes n *
        W ((Ideal.absNorm n : ℝ) / X) := byW:SmoothDyadicWeight ℂX:ℝ⊢ densityM W X = ∑' (n : Ideal 𝒪), outsideWeight 1 excludedPrimes n * W.toFun (↑(Ideal.absNorm n) / X)
  apply tsum_congrW:SmoothDyadicWeight ℂX:ℝ⊢ ∀ (b : Ideal 𝒪),
  (if ∀ P ∈ excludedPrimes, ¬P ∣ b then
      ↑(UniqueFactorizationMonoid.moebius b) * density b * W.toFun (↑(Ideal.absNorm b) / X)
    else 0) =
    outsideWeight 1 excludedPrimes b * W.toFun (↑(Ideal.absNorm b) / X)
  intro nW:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪⊢ (if ∀ P ∈ excludedPrimes, ¬P ∣ n then
    ↑(UniqueFactorizationMonoid.moebius n) * density n * W.toFun (↑(Ideal.absNorm n) / X)
  else 0) =
  outsideWeight 1 excludedPrimes n * W.toFun (↑(Ideal.absNorm n) / X)
  have hchi : (1 : DirichletCharacter ℂ 1) (Ideal.absNorm n) = 1 :=
    MulChar.one_apply (isUnit_of_subsingleton _)W:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1⊢ (if ∀ P ∈ excludedPrimes, ¬P ∣ n then
    ↑(UniqueFactorizationMonoid.moebius n) * density n * W.toFun (↑(Ideal.absNorm n) / X)
  else 0) =
  outsideWeight 1 excludedPrimes n * W.toFun (↑(Ideal.absNorm n) / X)
  simp only [outsideWeight, FiniteSFactor.outsideWeight, weightedMoebius,
    baseChangeWeight, hchi, mul_one, density, totientDensity]W:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1⊢ (if ∀ P ∈ excludedPrimes, ¬P ∣ n then
    (↑(UniqueFactorizationMonoid.moebius n) *
        ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))) *
      W.toFun (↑(Ideal.absNorm n) / X)
  else 0) =
  (if ∀ P ∈ excludedPrimes, ¬P ∣ n then
      ↑(UniqueFactorizationMonoid.moebius n) * ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))
    else 0) *
    W.toFun (↑(Ideal.absNorm n) / X)
  split_ifsposW:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1h✝:∀ P ∈ excludedPrimes, ¬P ∣ n⊢ (↑(UniqueFactorizationMonoid.moebius n) * ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))) *
    W.toFun (↑(Ideal.absNorm n) / X) =
  (↑(UniqueFactorizationMonoid.moebius n) * ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))) *
    W.toFun (↑(Ideal.absNorm n) / X)negW:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1h✝:¬∀ P ∈ excludedPrimes, ¬P ∣ n⊢ 0 = 0 * W.toFun (↑(Ideal.absNorm n) / X) <;>posW:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1h✝:∀ P ∈ excludedPrimes, ¬P ∣ n⊢ (↑(UniqueFactorizationMonoid.moebius n) * ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))) *
    W.toFun (↑(Ideal.absNorm n) / X) =
  (↑(UniqueFactorizationMonoid.moebius n) * ∏ P ∈ IdealMobiusDivisorSum.primeSupport n, (1 - 1 / ↑(Ideal.absNorm P))) *
    W.toFun (↑(Ideal.absNorm n) / X)negW:SmoothDyadicWeight ℂX:ℝn:Ideal 𝒪hchi:1 ↑(Ideal.absNorm n) = 1h✝:¬∀ P ∈ excludedPrimes, ¬P ∣ n⊢ 0 = 0 * W.toFun (↑(Ideal.absNorm n) / X) simpAll goals completed! 🐙

The unconditional amplified bound, with the same [1/2,1] smooth weight as the family and with its density coefficient visible in densityM.

theorem densityM_bound (W : SmoothDyadicWeight ℂ) (ε : ℝ) (hε : 0 < ε) :
    (fun X : ℝ ↦ densityM W X) =O[atTop]
      (fun X : ℝ ↦ X ^ ((11 / 12 : ℝ) + ε)) := byW:SmoothDyadicWeight ℂε:ℝhε:0 < ε⊢ (fun X => densityM W X) =O[atTop] fun X => X ^ (11 / 12 + ε)
  simpa only [densityM_eq_outsideWeight] using
    actual_smoothedWeightedMobiusBound 1 (1 : DirichletCharacter ℂ 1)
      W W.contDiff W.support_subset ε hεAll goals completed! 🐙

endend ElevenTwelfths.Zeta