AngularPrimitiveDualMoments.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cubic second moments for the actual primitive ideal characters. The primes above three are separated exactly before applying the cubic sieve.

lemma OAI.CubicFirstMoment.angularResidueIdealChar_primaryNormalize line 14
lemma OAI.CubicFirstMoment.angular_primitive_ideal_mixed_match line 25
Source documentation
Unit compatibility makes the angular coefficient independent of the chosen generator, also at primes common to the conductor.
```
lemma angular_primitive_ideal_mixed_match {a b d : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (ψ : MulChar (Residues d) ℂ) (ℓ : ℤ)
    (hu : AngularUnitCompatible d ψ ℓ)
    (hagree : ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
      ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x)
    (ν : EisensteinIdealExponent) (hν : primary (idealPrimaryGenerator ν)) :
    angularResidueIdealChar d ψ ℓ ν =
      theta ℓ (idealPrimaryGenerator ν)*primaryMixedIdealChar a b ν := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.AngularUnitCompatible, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealPrimaryGenerator, OAI.CubicFirstMoment.angularResidueIdealChar, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.primaryMixedIdealChar
lemma OAI.CubicFirstMoment.angularPrimitiveDualPolynomial_ramified_partition line 46

theorem OAI.CubicFirstMoment.normalized_angular_primitive_ideal_cubic_moment line 70

Source documentation

A family of primitive mixed characters satisfies the cubic second moment on a full ideal dyad. Only the explicit number of ramified parts is lost.

theorem normalized_angular_primitive_ideal_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset Eisenstein) (S : Finset EisensteinIdealExponent)
      (b : Eisenstein) (d : Eisenstein → Eisenstein)
      (ψ : (a : Eisenstein) → MulChar (Residues (d a)) ℂ) (ℓ : ℤ) (N J u : ℝ),
      primary b → Squarefree b → 1 ≤ N → 1 ≤ J →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N ∧ IsCoprime a b) →
      (∀ a ∈ P, d a ≠ 0) →
      (∀ a ∈ P, AngularUnitCompatible (d a) (ψ a) ℓ) →
      (∀ a ∈ P, ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
        ψ a (Ideal.Quotient.mk (modulus (d a)) x) = mixedCubic a b x) →
      (∀ ν ∈ S, J ≤ idealExponentNorm ν ∧ idealExponentNorm ν ≤ 2*J) →
      (∑ a ∈ P, ‖normalizedDualPolynomial S (angularResidueIdealChar (d a) (ψ a) ℓ)
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.AngularUnitCompatible, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.angularResidueIdealChar