ElevenTwelfths.ZetaFamily

ElevenTwelfths
ZetaFamily

import ElevenTwelfths.ConcreteFamily
import ElevenTwelfths.ActualFixedShellModels
import OAI.NumberTheory.DirichletL.MeanSquare.ThetaDensity
import OAI.NumberTheory.DirichletL.Mellin.SixthPowerAverage

The zeta family in the notation of the blueprint

These are concrete sums, not a structure of conjectural analytic inputs. The excluded primes are fixed once and for all at conductor one. The finite element sums are definitionally the existing public family; the theorem mean_square connects them to the actual theta construction and descent.

X and H are natural norm bounds. The estimate holds for H ≤ X^(1+θ); taking H comparable to that radius gives S(X,H) ≪ X H X^ε. We do not claim that bound uniformly for tiny H.

namespace ElevenTwelfths.Zetanoncomputable sectionopen scoped BigOperators Classicalopen OAIopen OAI.ActualEisensteinCubicopen OAI.CompletedGaussopen OAI.ConcretePrimeRowBridgeopen OAI.InitialMeanSquareopen OAI.ShortDraftHeckeBridgeopen OAI.CanonicalRowCompletionopen OAI.CanonicalCoefficientClassopen OAI.CubicEisenstein

The fixed finite exceptional set for zeta, not a varying conductor.

abbrev excludedPrimes : Finset (Ideal 𝒪) := reflectionExcludedPrimes 1abbrev columns (X : ℕ) : Finset 𝒪 := outsidePrimaryBall excludedPrimes Xabbrev rows (H : ℕ) : Finset 𝒪 := exactRowBall H

χ_n(h), the actual sextic character used in this finite column family.

abbrev sexticTwist (X : ℕ) (n h : 𝒪) : ℂ :=
  outsideSexticTwist excludedPrimes (reflectionExcludedPrimes_bad 1) X h n

The four visible ingredients: primaryness, Möbius, sextic twist, cutoff.

def M (W : SmoothDyadicWeight ℂ) (h : 𝒪) (X : ℕ) : ℂ :=
  ∑ n ∈ columns X, if primary n then
    (μ_K n : ℂ) * sexticTwist X n h * W ((𝒩 n : ℝ) / X) else 0

The untwisted Möbius sum M(X) from the intro.

def untwistedM (W : SmoothDyadicWeight ℂ) (X : ℕ) : ℂ :=
  ∑ n ∈ columns X, if primary n then
    (μ_K n : ℂ) * W ((𝒩 n : ℝ) / X) else 0

The smoothly weighted finite second moment.

def S (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff) (X H : ℕ) : ℝ :=
  ∑ h ∈ rows H, V ((𝒩 h : ℝ) / H) * ‖M W h X‖ ^ 2

theorem M_eq_outsideM (W : SmoothDyadicWeight ℂ) (h : 𝒪) (X : ℕ) :
    M W h X = outsideM excludedPrimes (reflectionExcludedPrimes_bad 1) W h X := rfl

theorem S_eq_outsideS (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff)
    (X H : ℕ) :
    S W V X H = outsideS excludedPrimes (reflectionExcludedPrimes_bad 1) W V X H := rfl

theorem M_one (W : SmoothDyadicWeight ℂ) (X : ℕ) :
    M W 1 X = untwistedM W X := byW:SmoothDyadicWeight ℂX:ℕ⊢ M W 1 X = untwistedM W X
  simp only [M, untwistedM, sexticTwist, outsideSexticTwist, idealSexticRow_one,
    mul_one]All goals completed! 🐙

Exact amplifier identity: sixth powers leave precisely a coprimality restriction. No prime-counting or asymptotic approximation is hidden here.

theorem M_sixth_power (W : SmoothDyadicWeight ℂ) (b : 𝒪) (X : ℕ) :
    M W (b ^ 6) X =
      ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
        (UniqueFactorizationMonoid.moebius n : ℂ) * W ((Ideal.absNorm n : ℝ) / X) := byW:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ M W (b ^ 6) X =
  ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
    ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)
  rw [M_eq_outsideM,W:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ outsideM excludedPrimes ⋯ W (b ^ 6) X =
  ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
    ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X) outsideM_eq_idealRowSum,W:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ idealRowSum (outsideIdealsUpTo excludedPrimes X) ⋯ ⋯ 1 (fun n => W.toFun (↑n / ↑X)) (b ^ 6) =
  ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
    ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)
    OAI.SixthPowerAverage.idealRowSum_sixth_eq_coprime_sumW:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ ∑ I ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime I (Ideal.span {b}),
    baseChangeWeight 1 I * W.toFun (↑(Ideal.absNorm I) / ↑X) =
  ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
    ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)]W:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ ∑ I ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime I (Ideal.span {b}),
    baseChangeWeight 1 I * W.toFun (↑(Ideal.absNorm I) / ↑X) =
  ∑ n ∈ outsideIdealsUpTo excludedPrimes X with IsCoprime n (Ideal.span {b}),
    ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)
  apply Finset.sum_congr rflW:SmoothDyadicWeight ℂb:𝒪X:ℕ⊢ ∀ x ∈ {I ∈ outsideIdealsUpTo excludedPrimes X | IsCoprime I (Ideal.span {b})},
  baseChangeWeight 1 x * W.toFun (↑(Ideal.absNorm x) / ↑X) =
    ↑(UniqueFactorizationMonoid.moebius x) * W.toFun (↑(Ideal.absNorm x) / ↑X)
  intro n hIW:SmoothDyadicWeight ℂb:𝒪X:ℕn:Ideal ActualEisensteinCubic.OhI:n ∈ {I ∈ outsideIdealsUpTo excludedPrimes X | IsCoprime I (Ideal.span {b})}⊢ baseChangeWeight 1 n * W.toFun (↑(Ideal.absNorm n) / ↑X) =
  ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)
  have hchi : (1 : DirichletCharacter ℂ 1) (Ideal.absNorm n) = 1 :=
    MulChar.one_apply (isUnit_of_subsingleton _)W:SmoothDyadicWeight ℂb:𝒪X:ℕn:Ideal ActualEisensteinCubic.OhI:n ∈ {I ∈ outsideIdealsUpTo excludedPrimes X | IsCoprime I (Ideal.span {b})}hchi:1 ↑(Ideal.absNorm n) = 1⊢ baseChangeWeight 1 n * W.toFun (↑(Ideal.absNorm n) / ↑X) =
  ↑(UniqueFactorizationMonoid.moebius n) * W.toFun (↑(Ideal.absNorm n) / ↑X)
  simp only [baseChangeWeight, hchi, mul_one]All goals completed! 🐙

The finite-to-lattice boundary immediately before applying Poisson.

theorem S_eq_tsum (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff)
    (X H : ℕ) :
    S W V X H = ∑' h : 𝒪, V ((𝒩 h : ℝ) / H) * ‖M W h X‖ ^ 2 :=
  outsideS_eq_tsum excludedPrimes (reflectionExcludedPrimes_bad 1) W V X H

The column coefficient with its smooth cutoff, before twisting.

def mobiusWeight (W : SmoothDyadicWeight ℂ) (X : ℕ) (n : 𝒪) : ℂ :=
  if primary n then (μ_K n : ℂ) * W ((𝒩 n : ℝ) / X) else 0

theorem M_eq_sum (W : SmoothDyadicWeight ℂ) (h : 𝒪) (X : ℕ) :
    M W h X = ∑ n ∈ columns X, mobiusWeight W X n * sexticTwist X n h := byW:SmoothDyadicWeight ℂh:𝒪X:ℕ⊢ M W h X = ∑ n ∈ columns X, mobiusWeight W X n * sexticTwist X n h
  apply Finset.sum_congr rflW:SmoothDyadicWeight ℂh:𝒪X:ℕ⊢ ∀ x ∈ columns X,
  (if primary x then ↑(μ_K x) * sexticTwist X x h * W.toFun (↑(𝒩 x) / ↑X) else 0) =
    mobiusWeight W X x * sexticTwist X x h
  intro n hnW:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns X⊢ (if primary n then ↑(μ_K n) * sexticTwist X n h * W.toFun (↑(𝒩 n) / ↑X) else 0) = mobiusWeight W X n * sexticTwist X n h
  simp only [mobiusWeight]W:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns X⊢ (if primary n then ↑(μ_K n) * sexticTwist X n h * W.toFun (↑(𝒩 n) / ↑X) else 0) =
  (if primary n then ↑(μ_K n) * W.toFun (↑(𝒩 n) / ↑X) else 0) * sexticTwist X n h
  split_ifsposW:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns Xh✝:primary n⊢ ↑(μ_K n) * sexticTwist X n h * W.toFun (↑(𝒩 n) / ↑X) = ↑(μ_K n) * W.toFun (↑(𝒩 n) / ↑X) * sexticTwist X n hnegW:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns Xh✝:¬primary n⊢ 0 = 0 * sexticTwist X n h <;>posW:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns Xh✝:primary n⊢ ↑(μ_K n) * sexticTwist X n h * W.toFun (↑(𝒩 n) / ↑X) = ↑(μ_K n) * W.toFun (↑(𝒩 n) / ↑X) * sexticTwist X n hnegW:SmoothDyadicWeight ℂh:𝒪X:ℕn:𝒪hn:n ∈ columns Xh✝:¬primary n⊢ 0 = 0 * sexticTwist X n h ringAll goals completed! 🐙

Open the square and reverse the finite sums: h is now inside. The complex cast on the real moment makes conjugation explicit. This is an exact identity, before diagonal removal or the coprime heuristic.

theorem S_open_square (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff)
    (X H : ℕ) :
    (S W V X H : ℂ) =
      ∑ n₁ ∈ columns X, ∑ n₂ ∈ columns X,
        mobiusWeight W X n₁ * star (mobiusWeight W X n₂) *
          ∑ h ∈ rows H, (V ((𝒩 h : ℝ) / H) : ℂ) *
            sexticTwist X n₁ h * star (sexticTwist X n₂ h) := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ⊢ ↑(S W V X H) =
  ∑ n₁ ∈ columns X,
    ∑ n₂ ∈ columns X,
      mobiusWeight W X n₁ * star (mobiusWeight W X n₂) *
        ∑ h ∈ rows H, ↑(V.toFun (↑(𝒩 h) / ↑H)) * sexticTwist X n₁ h * star (sexticTwist X n₂ h)
  conv_rhs => rw [Finset.sum_comm]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ| ∑ y ∈ columns X,
  ∑ x ∈ columns X,
    mobiusWeight W X x * star (mobiusWeight W X y) *
      ∑ h ∈ rows H, ↑(V.toFun (↑(𝒩 h) / ↑H)) * sexticTwist X x h * star (sexticTwist X y h)
  simp only [S, Complex.ofReal_sum, Complex.ofReal_mul, Complex.ofReal_pow,
    ← Complex.mul_conj', M_eq_sum, map_sum, Finset.sum_mul, Finset.mul_sum,
    map_mul]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ⊢ ∑ x ∈ rows H,
    ∑ x_1 ∈ columns X,
      ∑ i ∈ columns X,
        ↑(V.toFun (↑(𝒩 x) / ↑H)) *
          (mobiusWeight W X i * sexticTwist X i x *
            ((starRingEnd ℂ) (mobiusWeight W X x_1) * (starRingEnd ℂ) (sexticTwist X x_1 x))) =
  ∑ x ∈ columns X,
    ∑ x_1 ∈ columns X,
      ∑ i ∈ rows H,
        mobiusWeight W X x_1 * star (mobiusWeight W X x) *
          (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x_1 i * star (sexticTwist X x i))
  rw [Finset.sum_commW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ⊢ ∑ y ∈ columns X,
    ∑ x ∈ rows H,
      ∑ i ∈ columns X,
        ↑(V.toFun (↑(𝒩 x) / ↑H)) *
          (mobiusWeight W X i * sexticTwist X i x *
            ((starRingEnd ℂ) (mobiusWeight W X y) * (starRingEnd ℂ) (sexticTwist X y x))) =
  ∑ x ∈ columns X,
    ∑ x_1 ∈ columns X,
      ∑ i ∈ rows H,
        mobiusWeight W X x_1 * star (mobiusWeight W X x) *
          (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x_1 i * star (sexticTwist X x i))]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ⊢ ∑ y ∈ columns X,
    ∑ x ∈ rows H,
      ∑ i ∈ columns X,
        ↑(V.toFun (↑(𝒩 x) / ↑H)) *
          (mobiusWeight W X i * sexticTwist X i x *
            ((starRingEnd ℂ) (mobiusWeight W X y) * (starRingEnd ℂ) (sexticTwist X y x))) =
  ∑ x ∈ columns X,
    ∑ x_1 ∈ columns X,
      ∑ i ∈ rows H,
        mobiusWeight W X x_1 * star (mobiusWeight W X x) *
          (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x_1 i * star (sexticTwist X x i))
  apply Finset.sum_congr rflW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕ⊢ ∀ x ∈ columns X,
  ∑ x_1 ∈ rows H,
      ∑ i ∈ columns X,
        ↑(V.toFun (↑(𝒩 x_1) / ↑H)) *
          (mobiusWeight W X i * sexticTwist X i x_1 *
            ((starRingEnd ℂ) (mobiusWeight W X x) * (starRingEnd ℂ) (sexticTwist X x x_1))) =
    ∑ x_1 ∈ columns X,
      ∑ i ∈ rows H,
        mobiusWeight W X x_1 * star (mobiusWeight W X x) *
          (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x_1 i * star (sexticTwist X x i))
  intro n₁ hnW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns X⊢ ∑ x ∈ rows H,
    ∑ i ∈ columns X,
      ↑(V.toFun (↑(𝒩 x) / ↑H)) *
        (mobiusWeight W X i * sexticTwist X i x *
          ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x))) =
  ∑ x ∈ columns X,
    ∑ i ∈ rows H,
      mobiusWeight W X x * star (mobiusWeight W X n₁) *
        (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x i * star (sexticTwist X n₁ i))
  rw [Finset.sum_commW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns X⊢ ∑ y ∈ columns X,
    ∑ x ∈ rows H,
      ↑(V.toFun (↑(𝒩 x) / ↑H)) *
        (mobiusWeight W X y * sexticTwist X y x *
          ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x))) =
  ∑ x ∈ columns X,
    ∑ i ∈ rows H,
      mobiusWeight W X x * star (mobiusWeight W X n₁) *
        (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x i * star (sexticTwist X n₁ i))]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns X⊢ ∑ y ∈ columns X,
    ∑ x ∈ rows H,
      ↑(V.toFun (↑(𝒩 x) / ↑H)) *
        (mobiusWeight W X y * sexticTwist X y x *
          ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x))) =
  ∑ x ∈ columns X,
    ∑ i ∈ rows H,
      mobiusWeight W X x * star (mobiusWeight W X n₁) *
        (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x i * star (sexticTwist X n₁ i))
  apply Finset.sum_congr rflW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns X⊢ ∀ x ∈ columns X,
  ∑ x_1 ∈ rows H,
      ↑(V.toFun (↑(𝒩 x_1) / ↑H)) *
        (mobiusWeight W X x * sexticTwist X x x_1 *
          ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x_1))) =
    ∑ i ∈ rows H,
      mobiusWeight W X x * star (mobiusWeight W X n₁) *
        (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X x i * star (sexticTwist X n₁ i))
  intro n₂ hmW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns Xn₂:𝒪hm:n₂ ∈ columns X⊢ ∑ x ∈ rows H,
    ↑(V.toFun (↑(𝒩 x) / ↑H)) *
      (mobiusWeight W X n₂ * sexticTwist X n₂ x *
        ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x))) =
  ∑ i ∈ rows H,
    mobiusWeight W X n₂ * star (mobiusWeight W X n₁) *
      (↑(V.toFun (↑(𝒩 i) / ↑H)) * sexticTwist X n₂ i * star (sexticTwist X n₁ i))
  apply Finset.sum_congr rflW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns Xn₂:𝒪hm:n₂ ∈ columns X⊢ ∀ x ∈ rows H,
  ↑(V.toFun (↑(𝒩 x) / ↑H)) *
      (mobiusWeight W X n₂ * sexticTwist X n₂ x *
        ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ x))) =
    mobiusWeight W X n₂ * star (mobiusWeight W X n₁) *
      (↑(V.toFun (↑(𝒩 x) / ↑H)) * sexticTwist X n₂ x * star (sexticTwist X n₁ x))
  intro h huW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns Xn₂:𝒪hm:n₂ ∈ columns Xh:𝒪hu:h ∈ rows H⊢ ↑(V.toFun (↑(𝒩 h) / ↑H)) *
    (mobiusWeight W X n₂ * sexticTwist X n₂ h *
      ((starRingEnd ℂ) (mobiusWeight W X n₁) * (starRingEnd ℂ) (sexticTwist X n₁ h))) =
  mobiusWeight W X n₂ * star (mobiusWeight W X n₁) *
    (↑(V.toFun (↑(𝒩 h) / ↑H)) * sexticTwist X n₂ h * star (sexticTwist X n₁ h))
  simp only [starRingEnd_apply]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffX:ℕH:ℕn₁:𝒪hn:n₁ ∈ columns Xn₂:𝒪hm:n₂ ∈ columns Xh:𝒪hu:h ∈ rows H⊢ ↑(V.toFun (↑(𝒩 h) / ↑H)) *
    (mobiusWeight W X n₂ * sexticTwist X n₂ h * (star (mobiusWeight W X n₁) * star (sexticTwist X n₁ h))) =
  mobiusWeight W X n₂ * star (mobiusWeight W X n₁) *
    (↑(V.toFun (↑(𝒩 h) / ↑H)) * sexticTwist X n₂ h * star (sexticTwist X n₁ h))
  ringAll goals completed! 🐙

The actual analytic estimate, with no theta-model hypothesis left over. The row sum is the same M that appears in the definition of S.

theorem row_mean_square (W : SmoothDyadicWeight ℂ)
    (θ ε : ℝ) (hθ : 0 < θ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ X : ℕ, 1 ≤ X →
      ∀ T : Finset 𝒪,
      (∀ h ∈ T, (𝒩 h : ℝ) ≤ (X : ℝ) ^ (1 + θ)) →
      (∀ h ∈ T, h ≠ 0) →
      (∑ h ∈ T, ‖M W h X‖ ^ 2) ≤
        C * X * (X : ℝ) ^ (1 + θ) * (X : ℝ) ^ ε := byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ ∃ C,
  0 < C ∧
    ∀ (X : ℕ),
      1 ≤ X →
        ∀ (T : Finset 𝒪),
          (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  obtain ⟨C, hC, hmean⟩ := outside_mean_square_of_theta_models_pos
    (1 : DirichletCharacter ℂ 1) excludedPrimes
    (reflectionExcludedPrimes_bad 1) (reflectionExcludedPrimes_prime 1)
    1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor 1))
    (byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ 0 < 1 norm_numAll goals completed! 🐙) completedRamifiedStep_gt_one
    (reflectionLevelBound_ge_one 1 (byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ 1 ≠ 0 norm_numAll goals completed! 🐙))
    (actual_hasCanonicalThetaModels 1 (1 : DirichletCharacter ℂ 1))
    W (1 / 2) 1 (byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ 0 < 1 / 2 norm_numAll goals completed! 🐙) W.support_subset W.contDiff θ ε hθ hεW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset ActualEisensteinCubic.O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + θ)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo excludedPrimes D) ⋯ ⋯ 1 (fun n => W.toFun (↑n / Z)) z‖ ^ 2 ≤
              C * Z * Z ^ (1 + θ) * Z ^ ε⊢ ∃ C,
  0 < C ∧
    ∀ (X : ℕ),
      1 ≤ X →
        ∀ (T : Finset 𝒪),
          (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  refine ⟨C, hC, ?_⟩W:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset ActualEisensteinCubic.O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + θ)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo excludedPrimes D) ⋯ ⋯ 1 (fun n => W.toFun (↑n / Z)) z‖ ^ 2 ≤
              C * Z * Z ^ (1 + θ) * Z ^ ε⊢ ∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  intro X hX T hT hT0W:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset ActualEisensteinCubic.O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + θ)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo excludedPrimes D) ⋯ ⋯ 1 (fun n => W.toFun (↑n / Z)) z‖ ^ 2 ≤
              C * Z * Z ^ (1 + θ) * Z ^ εX:ℕhX:1 ≤ XT:Finset 𝒪hT:∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)hT0:∀ h ∈ T, h ≠ 0⊢ ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  simpa only [M_eq_outsideM, outsideM_eq_idealRowSum] using
    hmean X X (byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset ActualEisensteinCubic.O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + θ)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo excludedPrimes D) ⋯ ⋯ 1 (fun n => W.toFun (↑n / Z)) z‖ ^ 2 ≤
              C * Z * Z ^ (1 + θ) * Z ^ εX:ℕhX:1 ≤ XT:Finset 𝒪hT:∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)hT0:∀ h ∈ T, h ≠ 0⊢ 1 ≤ ↑X exact_mod_cast hXAll goals completed! 🐙) (byW:SmoothDyadicWeight ℂθ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (D : ℕ) (Z : ℝ),
  1 ≤ Z →
    1 * Z ≤ ↑D →
      ∀ (T : Finset ActualEisensteinCubic.O),
        (∀ z ∈ T, ↑(Ideal.absNorm (Ideal.span {z})) ≤ Z ^ (1 + θ)) →
          (∀ z ∈ T, z ≠ 0) →
            ∑ z ∈ T, ‖idealRowSum (outsideIdealsUpTo excludedPrimes D) ⋯ ⋯ 1 (fun n => W.toFun (↑n / Z)) z‖ ^ 2 ≤
              C * Z * Z ^ (1 + θ) * Z ^ εX:ℕhX:1 ≤ XT:Finset 𝒪hT:∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)hT0:∀ h ∈ T, h ≠ 0⊢ 1 * ↑X ≤ ↑X simpAll goals completed! 🐙) T hT hT0

Smooth second moment for a cutoff bounded by one. A general bounded cutoff can be rescaled; the column weight has no normalization assumption.

theorem mean_square (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff)
    (hV : ∀ t, V t ≤ 1) (θ ε : ℝ) (hθ : 0 < θ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ X H : ℕ, 1 ≤ X →
      (H : ℝ) ≤ (X : ℝ) ^ (1 + θ) →
      S W V X H ≤ C * X * (X : ℝ) ^ (1 + θ) * (X : ℝ) ^ ε := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  obtain ⟨C, hC, hmean⟩ := row_mean_square W θ ε hθ hεW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  refine ⟨C, hC, ?_⟩W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε⊢ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  intro X H hX hHW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)⊢ S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  have hzero : V 0 = 0 :=
    V.toSmoothDyadicWeight.eq_zero_of_lt_half (byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)⊢ 0 < 1 / 2 norm_numAll goals completed! 🐙)W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0⊢ S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  have hremove : S W V X H =
      ∑ h ∈ rowNormDisk H, V ((𝒩 h : ℝ) / H) * ‖M W h X‖ ^ 2 := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
    simp [S, rows, exactRowBall, Finset.sum_insert, mem_rowNormDisk, hzero]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  rw [hremoveW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε]W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  apply le_trans (Finset.sum_le_sum fun h hu ↦
    mul_le_of_le_one_left (sq_nonneg _) (hV _))W:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∑ i ∈ rowNormDisk H, ‖M W i X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε
  apply hmean X hXaW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∀ h ∈ rowNormDisk H, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)aW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∀ h ∈ rowNormDisk H, h ≠ 0
  ·aW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∀ h ∈ rowNormDisk H, ↑(𝒩 h) ≤ ↑X ^ (1 + θ) intro h huaW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2h:𝒪hu:h ∈ rowNormDisk H⊢ ↑(𝒩 h) ≤ ↑X ^ (1 + θ)
    exact (show (𝒩 h : ℝ) ≤ H byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε exact_mod_cast (mem_rowNormDisk.mp hu).2All goals completed! 🐙).trans hH
  ·aW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2⊢ ∀ h ∈ rowNormDisk H, h ≠ 0 intro h hu hzeroaW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero✝:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2h:𝒪hu:h ∈ rowNormDisk Hhzero:h = 0⊢ False
    have := (mem_rowNormDisk.mp hu).1aW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X : ℕ),
  1 ≤ X →
    ∀ (T : Finset 𝒪),
      (∀ h ∈ T, ↑(𝒩 h) ≤ ↑X ^ (1 + θ)) → (∀ h ∈ T, h ≠ 0) → ∑ h ∈ T, ‖M W h X‖ ^ 2 ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ XhH:↑H ≤ ↑X ^ (1 + θ)hzero✝:V.toFun 0 = 0hremove:S W V X H = ∑ h ∈ rowNormDisk H, V.toFun (↑(𝒩 h) / ↑H) * ‖M W h X‖ ^ 2h:𝒪hu:h ∈ rowNormDisk Hhzero:h = 0this:0 < Ideal.absNorm (Ideal.span {h})⊢ False
    simp [hzero] at thisAll goals completed! 🐙

The introductory X H bound, with the intended choice of row scale made explicit. The constant absorbs the factor two in dyadic comparison.

theorem mean_square_dyadic (W : SmoothDyadicWeight ℂ) (V : SmoothDyadicCutoff)
    (hV : ∀ t, V t ≤ 1) (θ ε : ℝ) (hθ : 0 < θ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ X H : ℕ, 1 ≤ X →
      (H : ℝ) ≤ (X : ℝ) ^ (1 + θ) →
      (X : ℝ) ^ (1 + θ) ≤ 2 * H →
      S W V X H ≤ C * X * H * (X : ℝ) ^ ε := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → ↑X ^ (1 + θ) ≤ 2 * ↑H → S W V X H ≤ C * ↑X * ↑H * ↑X ^ ε
  obtain ⟨C, hC, hmean⟩ := mean_square W V hV θ ε hθ hεW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε⊢ ∃ C, 0 < C ∧ ∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → ↑X ^ (1 + θ) ≤ 2 * ↑H → S W V X H ≤ C * ↑X * ↑H * ↑X ^ ε
  refine ⟨2 * C, byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε⊢ 0 < 2 * C positivityAll goals completed! 🐙, ?_⟩
  intro X H hX hupper hlowerW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ Xhupper:↑H ≤ ↑X ^ (1 + θ)hlower:↑X ^ (1 + θ) ≤ 2 * ↑H⊢ S W V X H ≤ 2 * C * ↑X * ↑H * ↑X ^ ε
  calc
    S W V X H ≤ C * X * (X : ℝ) ^ (1 + θ) * (X : ℝ) ^ ε :=
      hmean X H hX hupper
    _ ≤ C * X * (2 * H) * (X : ℝ) ^ ε := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ Xhupper:↑H ≤ ↑X ^ (1 + θ)hlower:↑X ^ (1 + θ) ≤ 2 * ↑H⊢ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ ε ≤ C * ↑X * (2 * ↑H) * ↑X ^ ε gcongrAll goals completed! 🐙
    _ = (2 * C) * X * H * (X : ℝ) ^ ε := byW:SmoothDyadicWeight ℂV:SmoothDyadicCutoffhV:∀ (t : ℝ), V.toFun t ≤ 1θ:ℝε:ℝhθ:0 < θhε:0 < εC:ℝhC:0 < Chmean:∀ (X H : ℕ), 1 ≤ X → ↑H ≤ ↑X ^ (1 + θ) → S W V X H ≤ C * ↑X * ↑X ^ (1 + θ) * ↑X ^ εX:ℕH:ℕhX:1 ≤ Xhupper:↑H ≤ ↑X ^ (1 + θ)hlower:↑X ^ (1 + θ) ≤ 2 * ↑H⊢ C * ↑X * (2 * ↑H) * ↑X ^ ε = 2 * C * ↑X * ↑H * ↑X ^ ε ringAll goals completed! 🐙

endend ElevenTwelfths.Zeta