IdealCubicMoments.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The proved element sieves apply directly to complete ideal-indexed polynomials through the injective chosen-generator map.

lemma OAI.CubicFirstMoment.sum_ideal_generator_image line 14

theorem OAI.CubicFirstMoment.ideal_cubic_moment line 22

Source documentation

Cubic moments for complete ideal supports, including the prime above 3.

theorem ideal_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset Eisenstein) (S : Finset EisensteinIdealExponent)
      (N Y D : ℝ), 1 ≤ N → 1 ≤ Y → 0 ≤ D →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ ν ∈ S, idealExponentNorm ν ≤ Y) → ∀ v : EisensteinIdealExponent → ℂ,
      (∀ ν ∈ S, ‖v ν‖ ≤ D) →
      (∑ a ∈ P, ‖∑ ν ∈ S, v ν*cubicSymbol a (idealExponentGenerator ν)‖^2) ≤
        C*(N*Y)^ε*Y*(N+Y+(N*Y)^(2/3:ℝ))*D^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.idealExponentGenerator

theorem OAI.CubicFirstMoment.ideal_mixed_moment line 50

Source documentation

The ordinary mixed-character moment keeps its exact ideal coefficient energy.

theorem ideal_mixed_moment (hHuxley : HuxleyAdditiveLargeSieve)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset (Eisenstein × Eisenstein))
      (S : Finset EisensteinIdealExponent) (Q Y : ℝ), 1 ≤ Q → 1 ≤ Y →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ ν ∈ S, idealExponentNorm ν ≤ Y) → ∀ v : EisensteinIdealExponent → ℂ,
      (∑ p ∈ P, ‖∑ ν ∈ S, v ν*mixedCubic p.1 p.2 (idealExponentGenerator ν)‖^2) ≤
        C*Q^ε*(Q^2+Y)*∑ ν ∈ S, ‖v ν‖^2 := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.idealExponentGenerator

lemma OAI.CubicFirstMoment.normalizedDualPolynomial_cubic line 79

theorem OAI.CubicFirstMoment.normalized_ideal_cubic_moment line 92

Source documentation

Normalized cubic dual blocks have coefficients bounded by one, uniformly in their additional norm twist.

theorem normalized_ideal_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset Eisenstein) (S : Finset EisensteinIdealExponent)
      (N Y J u : ℝ), 1 ≤ N → 1 ≤ Y → 0 < J →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ ν ∈ S, J ≤ idealExponentNorm ν ∧ idealExponentNorm ν ≤ Y) →
      (∑ a ∈ P, ‖normalizedDualPolynomial S
        (fun ν => cubicSymbol a (idealExponentGenerator ν)) idealExponentNorm J u‖^2) ≤
        C*(N*Y)^ε*Y*(N+Y+(N*Y)^(2/3:ℝ)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.idealExponentGenerator