1. ElevenTwelfths
  2. SixthPowerMeanSquare
import OAI.NumberTheory.DirichletL.Mellin.SixthPowerAverage

From the sextic mean square to the 11 / 12 Möbius bound

This module is the direct sixth-power amplifier used after the analytic mean-square argument. The mean-square estimate is an explicit hypothesis.

For alpha = (1 + theta) / 6, average the rows A (b ^ 6) over Norm b \asymp X ^ alpha. Cauchy--Schwarz costs the square root of the number of rows, while the zero Fourier mode contributes a factor X ^ alpha. Thus

(2 + theta - alpha) / 2 = (11 + 5 * theta) / 12.

namespace ElevenTwelfthsnoncomputable sectionopen scoped BigOperators Classical SchwartzMap ContDiff Topologyopen Filter Asymptotics MeasureTheoryopen OAIopen OAI.ActualEisensteinCubicopen OAI.ConcretePrimeRowBridge hiding Oopen OAI.EisensteinSchwartzPoisson hiding Oopen OAI.ConcreteTraceCRT OAI.ShortDraftHeckeBridgeopen OAI.QuadraticInitialBound hiding Oopen OAI.InitialMeanSquareopen OAI.SixthPowerAverage

A symbolic-theta form of the sixth-power averaging argument.

The hypothesis hmean is the sole deep analytic input. It says that every finite collection of nonzero sextic rows of norm at most X ^ (1 + theta) has second moment O(X ^ (2 + theta + 2 * epsilon)). The conclusion is the smooth weighted Eisenstein--Möbius bound with exponent (11 + 5 * theta) / 12 + epsilon.

theorem outside_totient_moebius_bound_of_mean_square {q : ℕ} (chi : DirichletCharacter ℂ q) (S : Finset (Ideal OAI.ActualEisensteinCubic.O)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes ⊆ S) (W : ℝ → ℂ) (a b : ℝ) (_ha : 0 < a) (hsupport : Function.support W ⊆ Set.Icc a b) (hW : ContDiff ℝ ∞ W) (theta epsilon Cmean : ℝ) (htheta : 0 ≤ theta) (hepsilon : 0 < epsilon) (hCmean : 0 < Cmean) (hmean : ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ D → ∀ T : Finset OAI.ActualEisensteinCubic.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 * epsilon)) : ∃ C : ℝ, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W ((Ideal.absNorm n : ℝ) / X) * totientDensity n‖ ≤ C * X ^ (((11 + 5 * theta) / 12 : ℝ) + epsilon) := q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport W⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hW⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) Ws⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 b⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilon⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponent⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ G⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBound⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ Error⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Average⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alpha⊢ ∃ C, 0 < C ∧ ∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) refine ⟨C, div_pos (q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alpha⊢ 0 < Average + Error All goals completed! 🐙) hhat, ?_⟩ q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑D⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < X⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alpha⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ B⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < B⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S D⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ 768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon))⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ 768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon))haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponent⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponent⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponent⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponenthfactor:X ^ averageExponent = B * X ^ targetExponent⊢ ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ C * X ^ ((11 + 5 * theta) / 12 + epsilon) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponenthfactor:X ^ averageExponent = B * X ^ targetExponent⊢ B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ outsideIdealsUpTo S D, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ B * ‖paperRadialFourier (⇑V) 0‖ * (C * X ^ ((11 + 5 * theta) / 12 + epsilon)) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponenthfactor:X ^ averageExponent = B * X ^ targetExponent⊢ (Average + Error) * X ^ averageExponent = B * ‖paperRadialFourier (⇑V) 0‖ * (C * X ^ ((11 + 5 * theta) / 12 + epsilon)) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponenthfactor:X ^ averageExponent = B * X ^ targetExponent⊢ (Average + Error) * (B * X ^ targetExponent) = B * ‖paperRadialFourier (⇑V) 0‖ * (C * X ^ ((11 + 5 * theta) / 12 + epsilon)) q:ℕchi:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hbad:CanonicalQuadraticSieve.fixedBadPrimes ⊆ SW:ℝ → ℂa:ℝb:ℝ_ha:0 < ahsupport:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ Wtheta:ℝepsilon:ℝCmean:ℝhtheta:0 ≤ thetahepsilon:0 < epsilonhCmean:0 < Cmeanhmean:∀ (D : ℕ) (X : ℝ), 1 ≤ X → b * X ≤ ↑D → ∀ (T : Finset ActualEisensteinCubic.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 * epsilon)V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hVs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0hVhat:paperRadialFourier (⇑V) 0 ≠ 0Cerror:ℝhCerror:0 < Cerrorherror:∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (Ideal.absNorm I) ≠ 0 → ↑(Ideal.absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (Ideal.absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ Cerror * G * pvControl V * lengthScale ^ (1 + epsilon)hWcompact:HasCompactSupport WWs:𝓢(ℝ, ℂ) := hWcompact.toSchwartzMap hWG:ℝ := (SchwartzMap.seminorm ℝ 0 0) WssupportBound:ℝ := max 1 bError:ℝ := Cerror * G * pvControl V * supportBound ^ (1 + epsilon)Average:ℝ := √(768 * Cmean)alpha:ℝ := (1 + theta) / 6targetExponent:ℝ := (11 + 5 * theta) / 12 + epsilonaverageExponent:ℝ := alpha + targetExponentC:ℝ := (Average + Error) / ‖paperRadialFourier (⇑V) 0‖hG:0 ≤ GhSupportBound:1 ≤ supportBoundhError:0 ≤ ErrorhAverage:0 < Averagehhat:0 < ‖paperRadialFourier (⇑V) 0‖halpha:0 ≤ alphaD:ℕX:ℝhX:1 ≤ XhD:b * X ≤ ↑DhXpos:0 < XB:ℝ := X ^ alphahB:1 ≤ BhBpos:0 < BF:Finset (Ideal ConcretePrimeRowBridge.O) := outsideIdealsUpTo S DA:ActualEisensteinCubic.O → ℂ := idealRowSum F ⋯ ⋯ chi fun n => W (↑n / X)hBpower:B ^ 6 = X ^ (1 + theta)hsecondMoment:∑ h ∈ Finset.image (fun b => b ^ 6) (averagingRows B), ‖A h‖ ^ 2 ≤ Cmean * X ^ (2 + theta + 2 * epsilon)havgSquare:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ^ 2 ≤ (Average * X ^ averageExponent) ^ 2haverageIdentity:768 * B * (Cmean * X ^ (2 + theta + 2 * epsilon)) = (Average * X ^ averageExponent) ^ 2havg:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * A (b ^ 6)‖ ≤ Average * X ^ averageExponenthremainder:‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F n) (⇑V) B‖ ≤ Error * X ^ (1 + epsilon)herrorExponent:X ^ (1 + epsilon) ≤ X ^ averageExponenthmain:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / B) * idealRowSum F ⋯ ⋯ chi (fun n => W (↑n / X)) (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight chi I * W (↑(Ideal.absNorm I) / X) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) B‖hbound:B * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ n ∈ F, baseChangeWeight chi n * W (↑(Ideal.absNorm n) / X) * totientDensity n‖ ≤ (Average + Error) * X ^ averageExponenthfactor:X ^ averageExponent = B * X ^ targetExponent⊢ (Average + Error) * (B * X ^ ((11 + 5 * theta) / 12 + epsilon)) = B * ‖paperRadialFourier (⇑V) 0‖ * ((Average + Error) / ‖paperRadialFourier (⇑V) 0‖ * X ^ ((11 + 5 * theta) / 12 + epsilon)) All goals completed! 🐙endend ElevenTwelfths