MixedPrimitiveReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic reduction of the original primary mixed-character sum to complete primitive ideal sums. Every Euler rescaling is retained.

lemma OAI.CubicFirstMoment.primary_mixed_smooth_eq_ideal line 15

theorem OAI.CubicFirstMoment.primary_mixed_smooth_primitive_reduction line 42

Source documentation

No primitive-character or character-agreement assumption remains in this exact reduction. Primitivity, nonprincipality, unit-invariance and the conductor upper bound are all supplied by the arithmetic proofs.

theorem primary_mixed_smooth_primitive_reduction {a b : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (hnu : ¬ IsUnit (a*b))
    (W : ℝ → ℂ) (hW : HasCompactSupport W) {Z : ℝ} (hZ : 0 < Z) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ),
      d ≠ 0 ∧ PrimitiveResidueCharacter d ψ ∧ ψ ≠ 1 ∧
      normNat d ≤ normNat (3*(a*b)) ∧
      (∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u) = 1) ∧
      (∑' x : Eisenstein, if primary x then mixedCubic a b x*W (norm x/Z) else 0) =
        ∑ T ∈ (idealExponentOf (3*(a*b))).support.powerset,
          (-1:ℂ)^T.card*residueIdealChar d ψ (primeSetExponent T)*
            ∑' κ, residueIdealChar d ψ κ*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.primeSetExponent

theorem OAI.CubicFirstMoment.primary_mixed_smooth_ramified_euler line 63

Source documentation

The local conductor calculation reduces the Euler correction to the fixed primes above three, independently of the varying squarefree modulus.

theorem primary_mixed_smooth_ramified_euler {a b d : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (ψ : MulChar (Residues d) ℂ)
    (hu : ∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u) = 1)
    (hagree : ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
      ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) {Z : ℝ} (hZ : 0 < Z) :
    (∑' x : Eisenstein, if primary x then mixedCubic a b x*W (norm x/Z) else 0) =
      ∑ T ∈ ramifiedIdealPrimes.powerset, (-1:ℂ)^T.card*
        residueIdealChar d ψ (primeSetExponent T)*
          ∑' κ, residueIdealChar d ψ κ*
            W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.primeSetExponent, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.primary_mixed_smooth_primitive_ramified line 96