ElevenTwelfths.Unconditional

ElevenTwelfths
Unconditional

import ElevenTwelfths.ActualFixedShellModels
import ElevenTwelfths.Nonvanishing
import ElevenTwelfths.SixthPowerMeanSquare

The unconditional `11 / 12` zero-free half-plane

This file assembles three independent pieces:

the actual fixed-shell models copied at the lower BranchDecoding layer;

the arbitrary-positive-radius mean square;

the direct sixth-power average and Mellin nonvanishing bridge.

namespace ElevenTwelfthsnoncomputable sectionopen Filter Asymptoticsopen scoped BigOperators Topology Classicalopen OAIopen OAI.ActualEisensteinCubicopen OAI.CanonicalCoefficientClassopen OAI.CanonicalRowCompletionopen OAI.CompletedGauss hiding Oopen OAI.ConcretePrimeRowBridge hiding Oopen OAI.CubicEisenstein hiding Oopen OAI.InitialMeanSquare hiding Oopen OAI.ShortDraftHeckeBridge hiding Oopen OAI.SixthPowerAverage

Arbitrarily short mean-square radii, followed by sixth-power averaging, give the public [1 / 2, 1] smoothed Möbius estimate at 11 / 12.

For a requested loss epsilon, take the row-radius parameter theta = 6 epsilon / 5 and give the post-square-root mean-square bound the loss epsilon / 2. Then (11 + 5 theta) / 12 + epsilon / 2 = 11 / 12 + epsilon.

theorem smoothedWeightedMobiusBound_of_theta_models_pos
    {q : ℕ} (chi : DirichletCharacter ℂ q)
    (S : Finset (Ideal O))
    (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes ⊆ S)
    (hSp : ∀ P ∈ S, Prime P)
    (rho rowBase levelBound : ℝ)
    (hrho : 0 < rho) (hrowBase : 1 < rowBase) (hlevel : 1 ≤ levelBound)
    (hmodels : HasCanonicalThetaModels S
      (conjugateMonoid (normCharacter chi)) rho rowBase levelBound) :
    SmoothedWeightedMobiusBound chi S (11 / 12 : ℝ) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12)
  intro W hW hsupp epsilon hepsilonq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilon⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  let theta : ℝ := 6 * epsilon / 5q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  let averageLoss : ℝ := epsilon / 2q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  have htheta : 0 < theta := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12)
    dsimp only [theta]q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2⊢ 0 < 6 * epsilon / 5
    linarithq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < theta⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  have haverageLoss : 0 < averageLoss := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12)
    dsimp only [averageLoss]q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < theta⊢ 0 < epsilon / 2
    linarithq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLoss⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  obtain ⟨Cmean, hCmean, hmean⟩ :=
    outside_mean_square_of_theta_models_pos chi S hbad hSp
      rho rowBase levelBound hrho hrowBase hlevel hmodels
      W (1 / 2 : ℝ) 1 (byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLoss⊢ 0 < 1 / 2 norm_numAll goals completed! 🐙) hsupp hW theta epsilon htheta hepsilonq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilon⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  have hmean' : ∀ (D : ℕ) (X : ℝ), 1 ≤ X → 1 * X ≤ D →
      ∀ T : Finset O,
      (∀ h ∈ T, (Ideal.absNorm (Ideal.span {h}) : ℝ) ≤
        X ^ (1 + theta : ℝ)) →
      (∀ h ∈ T, h ≠ 0) →
      (∑ h ∈ T,
        ‖idealRowSum (outsideIdealsUpTo S D)
          (outsideIdealsUpTo_ne_bot S D) (outside_good S D hbad)
          chi (fun n ↦ W (n / X)) h‖ ^ 2) ≤
        Cmean * X ^ ((2 + theta : ℝ) + 2 * averageLoss) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12)
    intro D X hX hD T hT hT0q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0⊢ ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
  Cmean * X ^ (2 + theta + 2 * averageLoss)
    have hXpos : 0 < X := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12) linarithq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
  Cmean * X ^ (2 + theta + 2 * averageLoss)
    apply (hmean D X hX hD T hT hT0).trans_eqq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X * X ^ (1 + theta) * X ^ epsilon = Cmean * X ^ (2 + theta + 2 * averageLoss)
    calc
      Cmean * X * X ^ (1 + theta : ℝ) * X ^ epsilon =
          Cmean * (X ^ (1 : ℝ) * X ^ (1 + theta : ℝ) *
            X ^ epsilon) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X * X ^ (1 + theta) * X ^ epsilon = Cmean * (X ^ 1 * X ^ (1 + theta) * X ^ epsilon) rw [Real.rpow_oneq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X * X ^ (1 + theta) * X ^ epsilon = Cmean * (X * X ^ (1 + theta) * X ^ epsilon)]q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X * X ^ (1 + theta) * X ^ epsilon = Cmean * (X * X ^ (1 + theta) * X ^ epsilon); ringAll goals completed! 🐙
      _ = Cmean * X ^ (1 + (1 + theta) + epsilon) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * (X ^ 1 * X ^ (1 + theta) * X ^ epsilon) = Cmean * X ^ (1 + (1 + theta) + epsilon)
        rw [← Real.rpow_add hXpos,q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * (X ^ (1 + (1 + theta)) * X ^ epsilon) = Cmean * X ^ (1 + (1 + theta) + epsilon) ← Real.rpow_add hXposq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X ^ (1 + (1 + theta) + epsilon) = Cmean * X ^ (1 + (1 + theta) + epsilon)]All goals completed! 🐙
      _ = Cmean * X ^ ((2 + theta : ℝ) + 2 * averageLoss) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ Cmean * X ^ (1 + (1 + theta) + epsilon) = Cmean * X ^ (2 + theta + 2 * averageLoss)
        congr 2e_a.e_aq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ 1 + (1 + theta) + epsilon = 2 + theta + 2 * averageLoss
        dsimp only [averageLoss]e_a.e_aq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonD:ℕX:ℝhX:1 ≤ XhD:1 * X ≤ ↑DT:Finset OhT:∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)hT0:∀ h ∈ T, h ≠ 0hXpos:0 < X⊢ 1 + (1 + theta) + epsilon = 2 + theta + 2 * (epsilon / 2)
        ringq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  obtain ⟨C, hC, hfinite⟩ := outside_totient_moebius_bound_of_mean_square
    chi S hbad W (1 / 2 : ℝ) 1 (byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)⊢ 0 < 1 / 2 norm_numAll goals completed! 🐙) hsupp hW
    theta averageLoss Cmean htheta.le haverageLoss hCmean hmean'q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)⊢ (fun Z => ∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / Z)) =O[atTop] fun Z =>
  Z ^ (11 / 12 + epsilon)
  apply IsBigO.of_bound Cq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)⊢ ∀ᶠ (x : ℝ) in atTop,
  ‖∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / x)‖ ≤ C * ‖x ^ (11 / 12 + epsilon)‖
  filter_upwards [eventually_ge_atTop (1 : ℝ)] with X hXq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ X⊢ ‖∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / X)‖ ≤ C * ‖X ^ (11 / 12 + epsilon)‖
  have hXpos : 0 < X := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12) linarithq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < X⊢ ‖∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / X)‖ ≤ C * ‖X ^ (11 / 12 + epsilon)‖
  let D : ℕ := ⌈X⌉₊q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊⊢ ‖∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / X)‖ ≤ C * ‖X ^ (11 / 12 + epsilon)‖
  have hD : 1 * X ≤ (D : ℝ) := byq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBound⊢ SmoothedWeightedMobiusBound chi S (11 / 12)
    simpa only [one_mul, D] using (Nat.le_ceil X)q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑D⊢ ‖∑' (I : Ideal O), outsideWeight chi S I * W (↑(Ideal.absNorm I) / X)‖ ≤ C * ‖X ^ (11 / 12 + epsilon)‖
  rw [(ideal_weighted_hasSum chi S W 1 X hXpos
      (fun n hx ↦ (hsupp hx).2) D hD).tsum_eq,q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑D⊢ ‖∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤
  C * ‖X ^ (11 / 12 + epsilon)‖
    Real.norm_of_nonneg (Real.rpow_nonneg hXpos.le _)q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑D⊢ ‖∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤
  C * X ^ (11 / 12 + epsilon)]q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑D⊢ ‖∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤
  C * X ^ (11 / 12 + epsilon)
  have h := hfinite D X hX hDq:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑Dh:‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
  C * X ^ ((11 + 5 * theta) / 12 + averageLoss)⊢ ‖∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤
  C * X ^ (11 / 12 + epsilon)
  convert h using 1q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑Dh:‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
  C * X ^ ((11 + 5 * theta) / 12 + averageLoss)⊢ C * X ^ (11 / 12 + epsilon) = C * X ^ ((11 + 5 * theta) / 12 + averageLoss)
  all_goals
    dsimp only [theta, averageLoss]q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ ShSp:∀ P ∈ S, Prime Prho:ℝrowBase:ℝlevelBound:ℝhrho:0 < rhohrowBase:1 < rowBasehlevel:1 ≤ levelBoundhmodels:HasCanonicalThetaModels S (conjugateMonoid (normCharacter chi)) rho rowBase levelBoundW:ℝ → ℂhW:ContDiff ℝ (↑⊤) Whsupp:Function.support W ⊆ Set.Icc (1 / 2) 1epsilon:ℝhepsilon:0 < epsilontheta:ℝ := 6 * epsilon / 5averageLoss:ℝ := epsilon / 2htheta:0 < thetahaverageLoss:0 < averageLossCmean:ℝhCmean:0 < Cmeanhmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + theta)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / Z)) z‖ ^ 2 ≤
              Cmean * Z * Z ^ (1 + theta) * Z ^ epsilonhmean':∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ∀ (T : Finset O),
        (∀ h ∈ T, ↑(Ideal.absNorm (Ideal.span {h})) ≤ X ^ (1 + theta)) →
          (∀ h ∈ T, h ≠ 0) →
            ∑ h ∈ T, ‖idealRowSum (outsideIdealsUpTo S D) ⋯ ⋯ chi (fun n => W (↑n / X)) h‖ ^ 2 ≤
              Cmean * X ^ (2 + theta + 2 * averageLoss)C:ℝhC:0 < Chfinite:∀ (D : ℕ) (X : ℝ),
  1 ≤ X →
    1 * X ≤ ↑D →
      ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
        C * X ^ ((11 + 5 * theta) / 12 + averageLoss)X:ℝhX:1 ≤ XhXpos:0 < XD:ℕ := ⌈X⌉₊hD:1 * X ≤ ↑Dh:‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤
  C * X ^ ((11 + 5 * theta) / 12 + averageLoss)⊢ C * X ^ (11 / 12 + epsilon) = C * X ^ ((11 + 5 * (6 * epsilon / 5)) / 12 + epsilon / 2)
    ring_nfAll goals completed! 🐙

The actual fixed-shell construction supplies the canonical models needed by the arbitrary-positive-radius mean square.

theorem actual_smoothedWeightedMobiusBound
    (q : ℕ) [NeZero q] (chi : DirichletCharacter ℂ q) :
    SmoothedWeightedMobiusBound chi (reflectionExcludedPrimes q)
      (11 / 12 : ℝ) := byq:ℕinst✝:NeZero qchi:DirichletCharacter ℂ q⊢ SmoothedWeightedMobiusBound chi (reflectionExcludedPrimes q) (11 / 12)
  exact smoothedWeightedMobiusBound_of_theta_models_pos chi
    (reflectionExcludedPrimes q) (reflectionExcludedPrimes_bad q)
    (reflectionExcludedPrimes_prime q) 1 completedRamifiedStep
    (fixedCuspLevelBound (reflectionConductor q)) (byq:ℕinst✝:NeZero qchi:DirichletCharacter ℂ q⊢ 0 < 1 norm_numAll goals completed! 🐙)
    completedRamifiedStep_gt_one
    (reflectionLevelBound_ge_one q (NeZero.ne q))
    (actual_hasCanonicalThetaModels q chi)

Direct Dirichlet nonvanishing at 11 / 12, assembled from the actual fixed-shell models rather than from a pre-existing zero-free theorem.

theorem dirichletL_ne_zero_of_re_gt_elevenTwelfths
    (q : ℕ) [NeZero q] (chi : DirichletCharacter ℂ q)
    (z : ℂ) (hz : (11 / 12 : ℝ) < z.re)
    (hpole : ¬ (chi = 1 ∧ z = 1)) :
    chi.LFunction z ≠ 0 :=
  dirichletL_ne_zero_of_smoothedWeightedMobiusBound chi
    (reflectionExcludedPrimes q) (reflectionExcludedPrimes_prime q)
    (11 / 12 : ℝ) (byq:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qz:ℂhz:11 / 12 < z.rehpole:¬(chi = 1 ∧ z = 1)⊢ 0 < 11 / 12 norm_numAll goals completed! 🐙) (byq:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qz:ℂhz:11 / 12 < z.rehpole:¬(chi = 1 ∧ z = 1)⊢ 11 / 12 < 1 norm_numAll goals completed! 🐙)
    (actual_smoothedWeightedMobiusBound q chi) z hz hpole

The unconditional 11 / 12 zero-free half-plane for Riemann zeta.

theorem riemannZeta_ne_zero_of_re_gt_elevenTwelfths
    (z : ℂ) (hz : (11 / 12 : ℝ) < z.re) :
    riemannZeta z ≠ 0 :=
  riemannZeta_ne_zero_of_elevenTwelfths_weightedMobiusBound
    (reflectionExcludedPrimes 1) (reflectionExcludedPrimes_prime 1)
    (actual_smoothedWeightedMobiusBound 1 (1 : DirichletCharacter ℂ 1)) z hz

endend ElevenTwelfths

The unconditional 11 / 12 zero-free half-plane

The unconditional `11 / 12` zero-free half-plane