PrimeConvolutionBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform coefficient bounds for a bounded number of ordered prime factors.

lemma OAI.CubicFirstMoment.prime_tuple_range_subset line 16
Source documentation
Every prime in another tuple with the same product occurs in the reference tuple. This includes repeated primes.
```
lemma prime_tuple_range_subset (f g : ι → Eisenstein)
    (hf : ∀ i, primaryPrime (f i)) (hg : ∀ i, primaryPrime (g i))
    (hprod : (∏ i, g i) = ∏ i, f i) (i : ι) :
    g i ∈ Finset.univ.image f := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime
theorem OAI.CubicFirstMoment.prime_tuple_fiber_card line 28
Source documentation
The deliberately generous k^k bound avoids ordering conventions and is uniform in the norm and in all independent supports.
```
theorem prime_tuple_fiber_card (S : ι → Finset Eisenstein)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) (b : Eisenstein) :
    ((Fintype.piFinset S).filter (fun f => (∏ i, f i) = b)).card ≤
      (Fintype.card ι)^(Fintype.card ι) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime

theorem OAI.CubicFirstMoment.orderedConvolution_norm_bound line 59

Source documentation

The coefficient bound depends only on the number of prime factors and on their separate weight bounds, including for nonsquarefree products.

theorem orderedConvolution_norm_bound (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (M : ι → ℝ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p)
    (hM : ∀ i, 0 ≤ M i) (hw : ∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i)
    (b : Eisenstein) :
    ‖orderedConvolution S w b‖ ≤
      ((Fintype.card ι)^(Fintype.card ι):ℕ)*(∏ i, M i) := by
…

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

theorem OAI.CubicFirstMoment.convolutionError_norm_bound line 82

Source documentation

Removing nonsquarefree products never enlarges a coefficient; its error also obeys the same uniform coefficient bound.

theorem convolutionError_norm_bound (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (M : ι → ℝ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p)
    (hM : ∀ i, 0 ≤ M i) (hw : ∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i)
    (b : Eisenstein) :
    ‖orderedConvolution S w b-squarefreeConvolution S w b‖ ≤
      ((Fintype.card ι)^(Fintype.card ι):ℕ)*(∏ i, M i) := by
…

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