StructuredConvolution.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite ordered prime convolutions used in the exceptional moments. The weights are independent on the prime factors; the squarefree cutoff is exposed exactly as the repeated-prime discrepancy.

def OAI.CubicFirstMoment.orderedConvolutionSupport line 16
def OAI.CubicFirstMoment.orderedConvolution line 19
def OAI.CubicFirstMoment.squarefreeConvolution line 23

theorem OAI.CubicFirstMoment.orderedConvolution_sum line 28

Source documentation

Exact collection of the ordered tuples by their product.

theorem orderedConvolution_sum (S : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ)
    (χ : Eisenstein → ℂ) :
    (∑ b ∈ orderedConvolutionSupport S, orderedConvolution S w b * χ b) =
      ∑ f ∈ Fintype.piFinset S, (∏ i, w i (f i))*χ (∏ i, f i) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution

theorem OAI.CubicFirstMoment.orderedConvolution_mixedCubic line 47
Source documentation
The full independent convolution separates exactly against the primitive mixed character; no product cutoff is inserted in this identity.
```
theorem orderedConvolution_mixedCubic (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) {q₁ q₂ : Eisenstein}
    (h₁ : primary q₁) (h₂ : primary q₂) :
    (∑ b ∈ orderedConvolutionSupport S, orderedConvolution S w b * mixedCubic q₁ q₂ b) =
      ∏ i, ∑ p ∈ S i, w i p * mixedCubic q₁ q₂ p := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.mixedCubic
theorem OAI.CubicFirstMoment.squarefree_prime_tuple_iff line 58
Source documentation
A product of primary primes is squarefree exactly when the tuple has no repeated prime. The normalization to primary elements makes equality, rather than association, the correct repetition test.
```
theorem squarefree_prime_tuple_iff (f : ι → Eisenstein) (hf : ∀ i, primaryPrime (f i)) :
    Squarefree (∏ i, f i) ↔ Function.Injective f := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime

theorem OAI.CubicFirstMoment.squarefreeConvolution_discrepancy line 80

Source documentation

The part removed by the squarefree restriction is precisely the sum of tuples with repeated prime factors.

theorem squarefreeConvolution_discrepancy (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (χ : Eisenstein → ℂ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) :
    (∑ b ∈ orderedConvolutionSupport S,
      (orderedConvolution S w b-squarefreeConvolution S w b)*χ b) =
      ∑ f ∈ Fintype.piFinset S with ¬Function.Injective f,
        (∏ i, w i (f i))*χ (∏ i, f i) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.squarefreeConvolution