ElevenTwelfths.ThetaSums

ElevenTwelfths
ThetaSums

import ElevenTwelfths.SmoothDyadic
import OAI.NumberTheory.DirichletL.GaussSum.CompletedExpansion
import OAI.NumberTheory.DirichletL.QuadraticSieve.LogarithmicLoss

Cubic completion and quadratic energy in readable notation

These interfaces reuse the upstream coefficients and the sharp sieve, rather than inventing coefficients with the desired properties. In particular the angular phase in c₃ and the square-root normalization in completion remain visible. A completed sum is NOT asserted to equal the original sum: the cube-inversion theorem gives the actual relation.

namespace ElevenTwelfths.Thetanoncomputable sectionopen scoped BigOperators Classicalopen OAI OAI.ActualEisensteinCubicopen OAI.CompletedGauss hiding O

The squarefree cubic Gauss coefficient, including its angular phase.

abbrev c₃ (I : Ideal O) : ℂ := squarefreeGaussCoefficient I

theorem c₃_eq (I : Ideal O) (hsq : Squarefree I)
    (hI : primaryGenerator I ≠ 0) :
    c₃ I = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI :=
  squarefreeGaussCoefficient_eq I hsq hI

The squarefree coefficient sum, with the twist Ψ exposed.

def cubicSum (Ψ : O →* ℂ) (W : SmoothDyadicWeight ℂ) (X : ℝ) : ℂ :=
  ∑' n : Ideal O, c₃ n * Ψ (primaryGenerator n) * W ((Ideal.absNorm n : ℝ) / X)

Completion restores the cube multiples I J³, with their actual weights.

def thetaSum (Ψ : O →* ℂ) (W : SmoothDyadicWeight ℂ) (X : ℝ) : ℂ :=
  ∑' I : Ideal O, ∑' J : Ideal O,
    (c₃ I * Ψ (primaryGenerator I)) / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) *
      cubeWeight Ψ J *
      Vstar W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm J : ℝ) ^ 3 / X)

theorem thetaSum_eq_completedT (Ψ : O →* ℂ) (W : SmoothDyadicWeight ℂ) (X : ℝ) :
    thetaSum Ψ W X = completedT Ψ W X := rfl

Exact bridge from the original cubic sum to completed theta sums. The original sum is recovered at cube-divided scales, not by erasing weights.

theorem cubicSum_eq_cube_inversion (Ψ : O →* ℂ) (W : SmoothDyadicWeight ℂ)
    (X : ℝ) (hX : 0 < X) :
    (Real.sqrt X : ℂ)⁻¹ * cubicSum Ψ W X =
      ∑' J : Ideal O, (UniqueFactorizationMonoid.moebius J : ℂ) * cubeWeight Ψ J *
        thetaSum Ψ W (X / (Ideal.absNorm J : ℝ) ^ 3) :=
  completed_cube_inverse Ψ W
    (HasCompactSupport.of_support_subset_isCompact isCompact_Icc W.support_subset) X hX

open OAI.CanonicalQuadraticSieve hiding O

Quadratic character: exactly the cube of the singleton sextic row.

abbrev χ₂ (I : Ideal O) (u : O) : ℂ := quadraticRow I u

theorem χ₂_eq_sextic_cube (I : Ideal O) (hI : Admissible I) (u : O) :
    χ₂ I u =
      (OAI.ConcretePrimeRowBridge.idealSexticRow {I}
        (singletonPositive I hI) (singletonGood I hI) I u) ^ 3 := byI:Ideal OhI:Admissible Iu:O⊢ χ₂ I u = ConcretePrimeRowBridge.idealSexticRow {I} ⋯ ⋯ I u ^ 3
  exact dite_eq_left hIAll goals completed! 🐙

A block of the quadratic energy. Its column coefficients do not depend on the row ℓ; obtaining such blocks from reflection is a separate step.

def quadraticEnergy (rows cols : Finset (Ideal O)) (a : Ideal O → ℂ) : ℝ :=
  ∑ ℓ ∈ rows, ‖∑ y ∈ cols, a y * χ₂ y (primaryGenerator ℓ)‖ ^ 2

The SHARP L+Y estimate, not the initial L+Y² bound.

theorem quadratic_large_sieve (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ L Y : ℝ, 1 ≤ L → 1 ≤ Y →
      ∀ rows cols : Finset (Ideal O),
      (∀ ℓ ∈ rows, Admissible ℓ ∧ (Ideal.absNorm ℓ : ℝ) ≤ L) →
      (∀ y ∈ cols, Admissible y ∧ (Ideal.absNorm y : ℝ) ≤ Y) →
      ∀ a : Ideal O → ℂ,
      quadraticEnergy rows cols a ≤
        C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2 := byε:ℝhε:0 < ε⊢ ∃ C,
  0 < C ∧
    ∀ (L Y : ℝ),
      1 ≤ L →
        1 ≤ Y →
          ∀ (rows cols : Finset (Ideal O)),
            (∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ L) →
              (∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Y) →
                ∀ (a : Ideal O → ℂ), quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  obtain ⟨C, hC, hsieve⟩ := finite_family_quadratic_large_sieve ε hεε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m : Type ?u.94} {n : Type ?u.93} [inst : Fintype m] [inst_1 : Fintype n]
        (rows : m → Ideal CanonicalQuadraticSieve.O) (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2⊢ ∃ C,
  0 < C ∧
    ∀ (L Y : ℝ),
      1 ≤ L →
        1 ≤ Y →
          ∀ (rows cols : Finset (Ideal O)),
            (∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ L) →
              (∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Y) →
                ∀ (a : Ideal O → ℂ), quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  refine ⟨C, hC, ?_⟩ε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m : Type ?u.94} {n : Type ?u.93} [inst : Fintype m] [inst_1 : Fintype n]
        (rows : m → Ideal CanonicalQuadraticSieve.O) (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2⊢ ∀ (L Y : ℝ),
  1 ≤ L →
    1 ≤ Y →
      ∀ (rows cols : Finset (Ideal O)),
        (∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ L) →
          (∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Y) →
            ∀ (a : Ideal O → ℂ), quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  intro L Y hL hY rows cols hrows hcols aε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m : Type ?u.94} {n : Type ?u.93} [inst : Fintype m] [inst_1 : Fintype n]
        (rows : m → Ideal CanonicalQuadraticSieve.O) (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂ⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  have h := hsieve L Y hL hY
    (fun ℓ : rows ↦ (ℓ : Ideal O)) (fun y : cols ↦ (y : Ideal O))
    Subtype.val_injective Subtype.val_injective
    (fun ℓ ↦ hrows ℓ ℓ.property) (fun y ↦ hcols y y.property)
    (fun y ↦ a y)ε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂh:∑ i, ‖∑ j, quadraticRow (↑j) (primaryGenerator ↑i) * a ↑j‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ j, ‖a ↑j‖ ^ 2⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  have sum_rows (f : Ideal O → ℝ) :
      (∑ ℓ : rows, f ℓ) = ∑ ℓ ∈ rows, f ℓ :=
    (Finset.sum_subtype rows (fun _ ↦ Iff.rfl) f).symmε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂh:∑ i, ‖∑ j, quadraticRow (↑j) (primaryGenerator ↑i) * a ↑j‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ j, ‖a ↑j‖ ^ 2sum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓ⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  have sum_cols (f : Ideal O → ℂ) :
      (∑ y : cols, f y) = ∑ y ∈ cols, f y :=
    (Finset.sum_subtype cols (fun _ ↦ Iff.rfl) f).symmε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂh:∑ i, ‖∑ j, quadraticRow (↑j) (primaryGenerator ↑i) * a ↑j‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ j, ‖a ↑j‖ ^ 2sum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f y⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  have sum_norm :
      (∑ y : cols, ‖a y‖ ^ 2) = ∑ y ∈ cols, ‖a y‖ ^ 2 :=
    (Finset.sum_subtype cols (fun _ ↦ Iff.rfl) (fun y ↦ ‖a y‖ ^ 2)).symmε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂh:∑ i, ‖∑ j, quadraticRow (↑j) (primaryGenerator ↑i) * a ↑j‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ j, ‖a ↑j‖ ^ 2sum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f ysum_norm:∑ y, ‖a ↑y‖ ^ 2 = ∑ y ∈ cols, ‖a y‖ ^ 2⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  have inner (ℓ : rows) :
      (∑ y : cols, quadraticRow y (primaryGenerator ℓ) * a y) =
        ∑ y ∈ cols, quadraticRow y (primaryGenerator ℓ) * a y :=
    sum_cols (fun y ↦ quadraticRow y (primaryGenerator ℓ) * a y)ε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂh:∑ i, ‖∑ j, quadraticRow (↑j) (primaryGenerator ↑i) * a ↑j‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ j, ‖a ↑j‖ ^ 2sum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f ysum_norm:∑ y, ‖a ↑y‖ ^ 2 = ∑ y ∈ cols, ‖a y‖ ^ 2inner:∀ (ℓ : ↥rows),
  ∑ y, quadraticRow (↑y) (primaryGenerator ↑ℓ) * a ↑y = ∑ y ∈ cols, quadraticRow y (primaryGenerator ↑ℓ) * a y⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  simp only [inner, sum_norm] at hε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂsum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f ysum_norm:∑ y, ‖a ↑y‖ ^ 2 = ∑ y ∈ cols, ‖a y‖ ^ 2inner:∀ (ℓ : ↥rows),
  ∑ y, quadraticRow (↑y) (primaryGenerator ↑ℓ) * a ↑y = ∑ y ∈ cols, quadraticRow y (primaryGenerator ↑ℓ) * a yh:∑ x, ‖∑ y ∈ cols, quadraticRow y (primaryGenerator ↑x) * a y‖ ^ 2 ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  rw [sum_rows (fun ℓ ↦ ‖∑ y ∈ cols, quadraticRow y (primaryGenerator ℓ) * a y‖ ^ 2)ε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂsum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f ysum_norm:∑ y, ‖a ↑y‖ ^ 2 = ∑ y ∈ cols, ‖a y‖ ^ 2inner:∀ (ℓ : ↥rows),
  ∑ y, quadraticRow (↑y) (primaryGenerator ↑ℓ) * a ↑y = ∑ y ∈ cols, quadraticRow y (primaryGenerator ↑ℓ) * a yh:∑ ℓ ∈ rows, ‖∑ y ∈ cols, quadraticRow y (primaryGenerator ℓ) * a y‖ ^ 2 ≤
  C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2] at hε:ℝhε:0 < εC:ℝhC:0 < Chsieve:∀ (M N : ℝ),
  1 ≤ M →
    1 ≤ N →
      ∀ {m n : Type} [inst : Fintype m] [inst_1 : Fintype n] (rows : m → Ideal CanonicalQuadraticSieve.O)
        (cols : n → Ideal CanonicalQuadraticSieve.O),
        Function.Injective rows →
          Function.Injective cols →
            (∀ (i : m), Admissible (rows i) ∧ ↑(Ideal.absNorm (rows i)) ≤ M) →
              (∀ (j : n), Admissible (cols j) ∧ ↑(Ideal.absNorm (cols j)) ≤ N) →
                ∀ (a : n → ℂ),
                  ∑ i, ‖∑ j, quadraticRow (cols j) (primaryGenerator (rows i)) * a j‖ ^ 2 ≤
                    C * (M * N) ^ ε * (M + N) * ∑ j, ‖a j‖ ^ 2L:ℝY:ℝhL:1 ≤ LhY:1 ≤ Yrows:Finset (Ideal O)cols:Finset (Ideal O)hrows:∀ ℓ ∈ rows, Admissible ℓ ∧ ↑(Ideal.absNorm ℓ) ≤ Lhcols:∀ y ∈ cols, Admissible y ∧ ↑(Ideal.absNorm y) ≤ Ya:Ideal O → ℂsum_rows:∀ (f : Ideal O → ℝ), ∑ ℓ, f ↑ℓ = ∑ ℓ ∈ rows, f ℓsum_cols:∀ (f : Ideal O → ℂ), ∑ y, f ↑y = ∑ y ∈ cols, f ysum_norm:∑ y, ‖a ↑y‖ ^ 2 = ∑ y ∈ cols, ‖a y‖ ^ 2inner:∀ (ℓ : ↥rows),
  ∑ y, quadraticRow (↑y) (primaryGenerator ↑ℓ) * a ↑y = ∑ y ∈ cols, quadraticRow y (primaryGenerator ↑ℓ) * a yh:∑ ℓ ∈ rows, ‖∑ y ∈ cols, quadraticRow y (primaryGenerator ℓ) * a y‖ ^ 2 ≤
  C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2⊢ quadraticEnergy rows cols a ≤ C * (L * Y) ^ ε * (L + Y) * ∑ y ∈ cols, ‖a y‖ ^ 2
  simpa only [quadraticEnergy, χ₂, mul_comm (a _) (quadraticRow _ _)] using hAll goals completed! 🐙

Algebra of the introductory sieve heuristic, conditional on its energy bound. This is NOT a theorem that the full reflected moment is one block.

theorem reflected_energy_bound (X H L Y E B : ℝ)
    (hX : 0 < X) (hH : 0 ≤ H) (hL : 0 < L)
    (hY : Y = L ^ 2 / X) (hE : E ≤ B * (L + Y) * Y) :
    (H * X / L ^ 2) * E ≤ B * H * (L + Y) := byX:ℝH:ℝL:ℝY:ℝE:ℝB:ℝhX:0 < XhH:0 ≤ HhL:0 < LhY:Y = L ^ 2 / XhE:E ≤ B * (L + Y) * Y⊢ H * X / L ^ 2 * E ≤ B * H * (L + Y)
  calc
    _ ≤ (H * X / L ^ 2) * (B * (L + Y) * Y) :=
      mul_le_mul_of_nonneg_left hE (byX:ℝH:ℝL:ℝY:ℝE:ℝB:ℝhX:0 < XhH:0 ≤ HhL:0 < LhY:Y = L ^ 2 / XhE:E ≤ B * (L + Y) * Y⊢ 0 ≤ H * X / L ^ 2 positivityAll goals completed! 🐙)
    _ = _ := byX:ℝH:ℝL:ℝY:ℝE:ℝB:ℝhX:0 < XhH:0 ≤ HhL:0 < LhY:Y = L ^ 2 / XhE:E ≤ B * (L + Y) * Y⊢ H * X / L ^ 2 * (B * (L + Y) * Y) = B * H * (L + Y) rw [hYX:ℝH:ℝL:ℝY:ℝE:ℝB:ℝhX:0 < XhH:0 ≤ HhL:0 < LhY:Y = L ^ 2 / XhE:E ≤ B * (L + Y) * Y⊢ H * X / L ^ 2 * (B * (L + L ^ 2 / X) * (L ^ 2 / X)) = B * H * (L + L ^ 2 / X)]X:ℝH:ℝL:ℝY:ℝE:ℝB:ℝhX:0 < XhH:0 ≤ HhL:0 < LhY:Y = L ^ 2 / XhE:E ≤ B * (L + Y) * Y⊢ H * X / L ^ 2 * (B * (L + L ^ 2 / X) * (L ^ 2 / X)) = B * H * (L + L ^ 2 / X); field_simpAll goals completed! 🐙

endend ElevenTwelfths.Theta