1. ElevenTwelfths
  2. Nonvanishing
import OAI.NumberTheory.DirichletL.RowCompletion.ThetaNonvanishingnamespace ElevenTwelfths

From the 11 / 12 Eisenstein--Möbius estimate to zeta nonvanishing

This file isolates the final analytic bridge. Its hypothesis is the smoothed weighted ideal sum produced by the sixth-power amplifier.

noncomputable sectionopen Filter Asymptoticsopen scoped BigOperators Topology ContDiffopen OAIopen OAI.ActualEisensteinCubicopen OAI.CanonicalRowCompletionopen OAI.CompactMellinBridgeopen OAI.ShortDraftHeckeBridge hiding Oopen OAI.SixthPowerAverage

The analytic-number-theory input needed by the final bridge.

For every smooth weight supported in the public dyadic interval [1 / 2, 1], the Eisenstein ideal sum with the finite bad Euler factors removed and with coefficient weightedMoebius = baseChangeWeight * totientDensity has exponent sigma + ε.

def SmoothedWeightedMobiusBound {q : ℕ} (chi : DirichletCharacter ℂ q) (S : Finset (Ideal O)) (sigma : ℝ) : Prop := ∀ (W : ℝ → ℂ), ContDiff ℝ ∞ W → Function.support W ⊆ Set.Icc (1 / 2 : ℝ) 1 → ∀ epsilon : ℝ, 0 < epsilon → (fun Z : ℝ ↦ ∑' I : Ideal O, outsideWeight chi S I * W ((Ideal.absNorm I : ℝ) / Z)) =O[atTop] (fun Z : ℝ ↦ Z ^ (sigma + epsilon))

Dilating a [1, 2] auxiliary weight by x ↦ 2x converts it to the public [1 / 2, 1] convention. The simultaneous scale change Z ↦ 2Z does not alter a power exponent.

theorem idealSum_isBigO_of_smoothedWeightedMobiusBound {q : ℕ} (chi : DirichletCharacter ℂ q) (S : Finset (Ideal O)) (sigma : ℝ) (hbound : SmoothedWeightedMobiusBound chi S sigma) (W : ℝ → ℂ) (hW : ContDiff ℝ ∞ W) (hsupp : ∀ x, x ≤ 1 ∨ 2 ≤ x → W x = 0) (epsilon : ℝ) (hepsilon : 0 < epsilon) : (fun Z : ℝ ↦ ∑' I : Ideal O, outsideWeight chi S I * W ((Ideal.absNorm I : ℝ) / Z)) =O[atTop] (fun Z : ℝ ↦ Z ^ (sigma + epsilon)) := q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilon⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ U⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ UhUsupp:Function.support U ⊆ Set.Icc (1 / 2) 1⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ UhUsupp:Function.support U ⊆ Set.Icc (1 / 2) 1hscaled:((fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / Z)) ∘ fun x => 2 * id x) =O[atTop] ((fun Z => Z ^ (sigma + epsilon)) ∘ fun x => 2 * id x)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ UhUsupp:Function.support U ⊆ Set.Icc (1 / 2) 1hscaled:((fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / Z)) ∘ fun x => 2 * id x) =O[atTop] ((fun Z => Z ^ (sigma + epsilon)) ∘ fun x => 2 * id x)hscaled':(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / (2 * Z))) =O[atTop] fun Z => (2 * Z) ^ (sigma + epsilon)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ UhUsupp:Function.support U ⊆ Set.Icc (1 / 2) 1hscaled:((fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / Z)) ∘ fun x => 2 * id x) =O[atTop] ((fun Z => Z ^ (sigma + epsilon)) ∘ fun x => 2 * id x)hscaled':(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / (2 * Z))) =O[atTop] fun Z => (2 * Z) ^ (sigma + epsilon)hleft:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / (2 * Z))) =ᶠ[atTop] fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonU:ℝ → ℂ := fun x => W (2 * x)hU:ContDiff ℝ ∞ UhUsupp:Function.support U ⊆ Set.Icc (1 / 2) 1hscaled:((fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / Z)) ∘ fun x => 2 * id x) =O[atTop] ((fun Z => Z ^ (sigma + epsilon)) ∘ fun x => 2 * id x)hscaled':(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / (2 * Z))) =O[atTop] fun Z => (2 * Z) ^ (sigma + epsilon)hleft:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * U (↑(Ideal.absNorm I) / (2 * Z))) =ᶠ[atTop] fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)hright:(fun Z => (2 * Z) ^ (sigma + epsilon)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon) All goals completed! 🐙

Rewrite the ideal-sum estimate in the weightedCompactSum form consumed by inverse Mellin continuation.

theorem weightedCompactSum_isBigO_of_smoothedWeightedMobiusBound {q : ℕ} (chi : DirichletCharacter ℂ q) (S : Finset (Ideal O)) (sigma : ℝ) (hbound : SmoothedWeightedMobiusBound chi S sigma) (W : ℝ → ℂ) (hW : ContDiff ℝ ∞ W) (hsupp : ∀ x, x ≤ 1 ∨ 2 ≤ x → W x = 0) (epsilon : ℝ) (hepsilon : 0 < epsilon) : (fun Z : ℝ ↦ weightedCompactSum chi S W Z⁻¹) =O[atTop] (fun Z : ℝ ↦ Z ^ (sigma + epsilon)) := q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilon⊢ (fun Z => weightedCompactSum chi S W Z⁻¹) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => weightedCompactSum chi S W Z⁻¹) =O[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =ᶠ[atTop] fun Z => weightedCompactSum chi S W Z⁻¹q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => Z ^ (sigma + epsilon)) =ᶠ[atTop] fun Z => Z ^ (sigma + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =ᶠ[atTop] fun Z => weightedCompactSum chi S W Z⁻¹ filter_upwards [eventually_ge_atTop (1 : ℝ)] with Z q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)Z:ℝhZ:1 ≤ Z⊢ ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z) = weightedCompactSum chi S W Z⁻¹ q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)Z:ℝhZ:1 ≤ Z⊢ weightedCompactSum chi S W Z⁻¹ = ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z) exact weightedCompactSum_eq_ideal_tsum chi S W Z 2 (q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)Z:ℝhZ:1 ≤ Z⊢ 0 < Z All goals completed! 🐙) (fun x hx ↦ q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)Z:ℝhZ:1 ≤ Zx:ℝhx:W x ≠ 0⊢ x ≤ 2 q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)Z:ℝhZ:1 ≤ Zx:ℝhx:W x ≠ 0h2:x < 2⊢ x ≤ 2 All goals completed! 🐙) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0epsilon:ℝhepsilon:0 < epsilonhideal:(fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z => Z ^ (sigma + epsilon)⊢ (fun Z => Z ^ (sigma + epsilon)) =ᶠ[atTop] fun Z => Z ^ (sigma + epsilon) All goals completed! 🐙

The smoothed weighted Möbius estimate gives analytic continuation of the inverse Mellin factor to re s > sigma.

theorem weightedCompactMellin_analytic_of_smoothedWeightedMobiusBound {q : ℕ} (chi : DirichletCharacter ℂ q) (S : Finset (Ideal O)) (sigma : ℝ) (hbound : SmoothedWeightedMobiusBound chi S sigma) (W : ℝ → ℂ) (hW : ContDiff ℝ ∞ W) (hsupp : ∀ x, x ≤ 1 ∨ 2 ≤ x → W x = 0) : AnalyticOnNhd ℂ (fun s : ℂ ↦ mellin (fun Z : ℝ ↦ weightedCompactSum chi S W Z⁻¹) (-s)) {s : ℂ | sigma < s.re} := q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0⊢ AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re} q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)⊢ AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re} q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volume⊢ AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re} q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0⊢ AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re} q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0s:ℂhs:s ∈ {s | sigma < s.re}⊢ AnalyticAt ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) s q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0s:ℂhs:s ∈ {s | sigma < s.re}hepsilon:0 < (s.re - sigma) / 2⊢ AnalyticAt ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) s q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0s:ℂhs:s ∈ {s | sigma < s.re}hepsilon:0 < (s.re - sigma) / 2⊢ s ∈ {s_1 | sigma + (s.re - sigma) / 2 < s_1.re} q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0s:ℂhs:s ∈ {s | sigma < s.re}hepsilon:0 < (s.re - sigma) / 2⊢ sigma + (s.re - sigma) / 2 < s.re q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)sigma:ℝhbound:SmoothedWeightedMobiusBound chi S sigmaW:ℝ → ℂhW:ContDiff ℝ ∞ Whsupp:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hsum:∀ (t : ℝ), 0 < t → HasSum (fun n => weightedCoeff chi S n * W (↑n * t)) (weightedCompactSum chi S W t)hlocal:MeasureTheory.LocallyIntegrableOn (fun D => weightedCompactSum chi S W D⁻¹) (Set.Ioi 0) MeasureTheory.volumehzero:(fun D => weightedCompactSum chi S W D⁻¹) =ᶠ[𝓝[>] 0] fun x => 0s:ℂhepsilon:0 < (s.re - sigma) / 2hs:sigma < s.re⊢ sigma + (s.re - sigma) / 2 < s.re All goals completed! 🐙

A direct per-character zero-free theorem from the sigma weighted Eisenstein--Möbius estimate.

theorem dirichletL_ne_zero_of_smoothedWeightedMobiusBound {q : ℕ} [NeZero q] (chi : DirichletCharacter ℂ q) (S : Finset (Ideal O)) (hS : ∀ P ∈ S, Prime P) (sigma : ℝ) (hsigma_pos : 0 < sigma) (hsigma : sigma < 1) (hbound : SmoothedWeightedMobiusBound chi S sigma) (z : ℂ) (hz : sigma < z.re) (hpole : ¬ (chi = 1 ∧ z = 1)) : chi.LFunction z ≠ 0 := q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1⊢ DirichletCharacter.LFunction chi z ≠ 0q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:¬z.re < 1⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight z⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ W⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}hE:AnalyticOnNhd ℂ (finiteEulerFactor chi S) {s | sigma < s.re}⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}hE:AnalyticOnNhd ℂ (finiteEulerFactor chi S) {s | sigma < s.re}hH:AnalyticOnNhd ℂ (SmoothMobiusCorrection.eulerCorrection chi S) {s | sigma < s.re}⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}hE:AnalyticOnNhd ℂ (finiteEulerFactor chi S) {s | sigma < s.re}hH:AnalyticOnNhd ℂ (SmoothMobiusCorrection.eulerCorrection chi S) {s | sigma < s.re}hWanalytic:AnalyticOnNhd ℂ (mellin W) {s | sigma < s.re}⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}hE:AnalyticOnNhd ℂ (finiteEulerFactor chi S) {s | sigma < s.re}hH:AnalyticOnNhd ℂ (SmoothMobiusCorrection.eulerCorrection chi S) {s | sigma < s.re}hWanalytic:AnalyticOnNhd ℂ (mellin W) {s | sigma < s.re}hnotboth:chi ≠ 1 ∨ baseChangeChar chi ≠ 1⊢ DirichletCharacter.LFunction chi z ≠ 0 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:z.re < 1W:ℝ → ℂ := ConcreteCompactWeight.weight zhW:ContDiff ℝ ∞ WhWs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0hM:AnalyticOnNhd ℂ (fun s => mellin (fun Z => weightedCompactSum chi S W Z⁻¹) (-s)) {s | sigma < s.re}hE:AnalyticOnNhd ℂ (finiteEulerFactor chi S) {s | sigma < s.re}hH:AnalyticOnNhd ℂ (SmoothMobiusCorrection.eulerCorrection chi S) {s | sigma < s.re}hWanalytic:AnalyticOnNhd ℂ (mellin W) {s | sigma < s.re}hnotboth:chi ≠ 1 ∨ baseChangeChar chi ≠ 1hzneq:z ≠ 1⊢ DirichletCharacter.LFunction chi z ≠ 0 All goals completed! 🐙 q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qS:Finset (Ideal O)hS:∀ P ∈ S, Prime Psigma:ℝhsigma_pos:0 < sigmahsigma:sigma < 1hbound:SmoothedWeightedMobiusBound chi S sigmaz:ℂhz:sigma < z.rehpole:¬(chi = 1 ∧ z = 1)hz1:¬z.re < 1⊢ DirichletCharacter.LFunction chi z ≠ 0 All goals completed! 🐙

The final bridge at the requested exponent. The hypothesis is only the smoothed weighted Eisenstein--Möbius bound for the trivial character modulo one and one finite set of prime Euler factors.

theorem riemannZeta_ne_zero_of_elevenTwelfths_weightedMobiusBound (S : Finset (Ideal O)) (hS : ∀ P ∈ S, Prime P) (hbound : SmoothedWeightedMobiusBound (1 : DirichletCharacter ℂ 1) S (11 / 12 : ℝ)) (z : ℂ) (hz : (11 / 12 : ℝ) < z.re) : riemannZeta z ≠ 0 := S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.re⊢ riemannZeta z ≠ 0 S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.rehz1:z = 1⊢ riemannZeta z ≠ 0S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.rehz1:¬z = 1⊢ riemannZeta z ≠ 0 S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.rehz1:z = 1⊢ riemannZeta z ≠ 0 All goals completed! 🐙 S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.rehz1:¬z = 1⊢ riemannZeta z ≠ 0 S:Finset (Ideal O)hS:∀ P ∈ S, Prime Phbound:SmoothedWeightedMobiusBound 1 S (11 / 12)z:ℂhz:11 / 12 < z.rehz1:¬z = 1hL:DirichletCharacter.LFunction 1 z ≠ 0⊢ riemannZeta z ≠ 0 All goals completed! 🐙endend ElevenTwelfths