PublishedHecke.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite-order Hecke prime input

The finite-order Hecke prime-sum input specializes to independent prime factors using the elementary character laws.

The input is the cubic-character consequence of Thorner--Zaman, A unified and improved Chebotarev density theorem, Algebra & Number Theory 13 (2019), Theorem 1.4, in the Siegel–Walfisz form for cubic Hecke characters. Only finite-order characters occur in this input; smooth weights and norm twists follow by partial summation.

def OAI.CubicFirstMoment.mixedCubic line 25
Source documentation
The primitive cubic characters occurring after cancelling common factors of two squarefree conductors.
```
def mixedCubic (q₁ q₂ a : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.mixedCubic_mul line 28
theorem OAI.CubicFirstMoment.mixedCubic_one line 34
theorem OAI.CubicFirstMoment.mixedCubic_norm_of_coprime line 40
def OAI.CubicFirstMoment.MixedCubicNonprincipal line 48
Source documentation
Excludes the principal character on ideals prime to the conductor.
```
def MixedCubicNonprincipal (q₁ q₂ : Eisenstein) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.CubicPrimeSiegelWalfisz line 56
Source documentation
Exact logarithmic-conductor prime-sum input. The conductor is the product of the coprime squarefree conductors of the two character factors. Constants are uniform over that family. Both conjugate primes are counted.
This is an explicit hypothesis type, not an asserted theorem.
```
def CubicPrimeSiegelWalfisz : Prop :=
…
```
theorem OAI.CubicFirstMoment.mixedCubic_prod line 69
Source documentation
The character of an ordered tuple splits into the characters of its individual factors. Repeated prime factors are still permitted here; the squarefree restriction in the manuscript is imposed separately.
```
theorem mixedCubic_prod {ι : Type*} (s : Finset ι) (f : ι → Eisenstein)
    {q₁ q₂ : Eisenstein} (h₁ : primary q₁) (h₂ : primary q₂) :
    mixedCubic q₁ q₂ (∏ i ∈ s, f i) = ∏ i ∈ s, mixedCubic q₁ q₂ (f i) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.mixedCubic

theorem OAI.CubicFirstMoment.independent_prime_tuple_character_sum line 80

Source documentation

Exact factorization of an independent prime-tuple character sum. The supports may be distinct smooth norm dyads, with their weights already included in w. No condition coupling the tuple's product is inserted.

theorem independent_prime_tuple_character_sum {ι : Type*} [Fintype ι] [DecidableEq ι]
    (supports : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ)
    {q₁ q₂ : Eisenstein} (h₁ : primary q₁) (h₂ : primary q₂) :
    (∑ f ∈ Fintype.piFinset supports,
      (∏ i, w i (f i)) * mixedCubic q₁ q₂ (∏ i, f i)) =
      ∏ i, ∑ p ∈ supports i, w i p * mixedCubic q₁ q₂ p := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.mixedCubic