SmallEulerProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Euler factor for a varying small modulus costs only an arbitrary positive power of its norm.

theorem OAI.CubicFirstMoment.supported_euler_small_power line 13
theorem OAI.CubicFirstMoment.supportedParts_card_small_power line 104
Source documentation
Uniform subpower counting of the actual supported parts.
```
theorem supportedParts_card_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (v : Eisenstein) (S : Finset EisensteinIdealExponent) (J : ℝ),
      v ≠ 0 → 1 ≤ J → (∀ ν ∈ S, idealExponentNorm ν ≤ J) →
      ((supportedParts v S).card:ℝ) ≤ C*(J*norm v)^ε := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.supportedParts, OAI.CubicFirstMoment.norm