PrimaryDualMoment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual cubic dual dyads. The conductor and root-number phases are outside the polynomials, and the dyadic loss is explicit.

lemma OAI.CubicFirstMoment.idealDyadIndex_scale_le line 14

theorem OAI.CubicFirstMoment.retained_primary_cubic_moment line 23

Source documentation

The retained integral for the actual primary-normalized characters has the predicted cubic second-moment size, with an explicit squared dyad count. The fixed local factor is an actual coefficient twist.

theorem retained_primary_cubic_moment {ε : ℝ} (hε : 0 < ε)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (P : Finset Eisenstein) (b : Eisenstein)
      (ξ : EisensteinIdealExponent → ℂ) (root : Eisenstein → ℂ)
      (A : Eisenstein → ℝ) (N J Z t : ℝ),
      primary b → (∀ ν, ‖ξ ν‖ ≤ 1) →
      (∀ a ∈ P, ‖root a‖ = 1) → (∀ a ∈ P, 0 < A a) →
      1 ≤ N → 1 ≤ J → 1 ≤ Z →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∑ a ∈ P, ‖finiteDualIntegral W (fullIdealBall J)
        (fun ν => ξ ν*primaryMixedIdealChar a b ν) idealExponentNorm (root a) (A a) Z t‖^2) ≤
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.finiteDualIntegral, OAI.CubicFirstMoment.fullIdealBall, OAI.CubicFirstMoment.primaryMixedIdealChar, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.full_smooth_primary_cubic_moment line 90

Source documentation

From the exact completed Hecke inputs, the full smooth sum inherits the explicit cubic dual bound and the arbitrarily small truncation error. The dual coefficients here are the actual primary-normalized characters.

theorem full_smooth_primary_cubic_moment {ε : ℝ} (hε : 0 < ε)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {δ : ℝ} (hδ : 0 < δ) (H R : ℝ) :
    ∃ C D : ℝ, 0 ≤ C ∧ 0 ≤ D ∧
      ∀ (P : Finset Eisenstein) (b : Eisenstein)
      (χ : Eisenstein → EisensteinIdealExponent → ℂ)
      (ξ : EisensteinIdealExponent → ℂ) (root : Eisenstein → ℂ)
      (A : Eisenstein → ℝ) (N Y Z J t : ℝ),
      primary b → (∀ a ∈ P, ∀ ν, ‖χ a ν‖ ≤ 1) → (∀ ν, ‖ξ ν‖ ≤ 1) →
      (∀ a ∈ P, ‖root a‖ = 1) → (∀ a ∈ P, 0 < A a) →
      1 ≤ N → 1 ≤ Y → 1 ≤ Z → 1 ≤ J → Z ≤ Y^H → J ≤ Y^H →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm